| #include <stdio.h> | |
| #include <stdlib.h> | |
| #define MEM_SIZE 1000000000 //10^9 | |
| struct mem_array { | |
| size_t buff_size; | |
| char * addr; | |
| }; |
| type term = | |
| | Var of int | |
| | Num of int | |
| | App of term * term | |
| | Lam of term | |
| | Plus of term * term | |
| | Ite of term * term * term | |
| type input = { mutable pos : int; mutable str : string } |
| Require Import Lia. | |
| Section Iter_to_ind. | |
| Variable B : Prop. | |
| Variable F : Prop -> Prop. | |
| Hypothesis F_ext : forall P Q, (P <-> Q) -> (F P <-> F Q). | |
| Fixpoint iter_prop (n : nat) : Prop := |
| Notation "P ≢ Q" := (~(P <-> Q))(at level 100). | |
| Theorem no_middle : ~(exists P, (P ≢ True) /\ (P ≢ False)). | |
| Proof. | |
| intro h. | |
| destruct h as [P [h1 h2]]. | |
| apply h2. | |
| split; [ | intros h; contradiction]. | |
| intros h3. | |
| apply h1; split; auto. |
| Require Import Setoid. | |
| Axiom is_a_neg : forall (P : Prop), exists (Q : Prop), P <-> ~Q. | |
| Lemma not_not : forall P, ~~P -> P. | |
| Proof. | |
| intros P. | |
| assert (h := is_a_neg P); destruct h as [Q h]. | |
| rewrite h. |
| (* A relatively straightforward formalization of HA^2 *) | |
| Require Import Coq.Lists.List. | |
| Require Import Coq.Strings.String. | |
| Inductive tm := | |
| | v(name : string) | |
| | Succ(a : tm) | |
| | Z | |
| | Plus(a b : tm) |
| (* | |
| Ideas: | |
| I'm borrowing generously from https://xavierleroy.org/talks/compilation-agay.pdf and | |
| https://github.com/ajcave/code/blob/master/normalization/weak-head-bigstep-cbn.agda | |
| But CBV. | |
| *) |
| (* | |
| Ideas: | |
| 1. Strong reduction (ugh): Keep computing through lambdas. Most straightforward, but annoying, need to reason about db even more | |
| 2. Computability take an eval context as well, so that all predicates are "up to substitution". | |
| Problem: how to we deal with "computable contexts"? | |
| E.g. aplications: Do they thake the previous elements in the env or not? | |
| Does "positive" style predicates help? | |
| 3. Screw this and go with names. | |
| 4. Reason about only closed terms (somehow?) Not sure how to formulate the main lemma. |
Confluence. It's not just a place where you can complain about colleagues to other colleagues.
It's also a property that is quite useful in many areas of CS!
As a reminder, a (non-deterministic) reduction relation --> is confluent if for every (multi-step) "peak"
u *<-- t -->* v (I use -->* for the multi-step version of -->) there is a corresponding "valley":
u -->* w *<-- v.
This basically says that your computation can't be "too"
| Set Implicit Arguments. | |
| (* On importe le module qui definit les listes *) | |
| Require Import List. | |
| Print list. | |
| Print option. | |
| (* Une section permet de declarer des Hypotheses et des Variables *) | |
| Section Typer. |