diff --git a/lambda.v b/lambda.v index ee83e3a..8c3de9d 100644 --- a/lambda.v +++ b/lambda.v @@ -4,64 +4,51 @@ Import Nat. Require Import Lists.List. Import ListNotations. +Require Import Setoid. +Require Import Relation_Definitions. +Require Import Morphisms. + +Require Import Relations.Relation_Operators. + Inductive type : Set := | tyvar : nat -> type -| arrow : type -> type -> type. +| tyfree : nat -> type +| arrow : type -> type -> type +| pi : type -> type. Scheme Equality for type. Inductive term : Set := | var : nat -> term | free : nat -> term -| app : term -> term -> term -| abs : type -> term -> term. +| app1 : term -> term -> term +| app2 : term -> type -> term +| abs1 : type -> term -> term +| abs2 : term -> term. Declare Custom Entry lambda. Notation "<{ e }>" := e (e custom lambda at level 99). Notation "( x )" := x (in custom lambda, x at level 99). +Notation "< x >" := (tyvar x) (in custom lambda, x at level 99). Notation "{ x }" := x (x at level 99). Notation "x" := x (in custom lambda at level 0, x constr at level 0). Notation "S -> T" := (arrow S T) (in custom lambda at level 50, right associativity). -Notation "x y" := (app x y) (in custom lambda at level 1, left associativity). +Notation "'Π' b" := + (pi b) (in custom lambda at level 90, + b custom lambda at level 99, left associativity). +Notation "x · y" := (app1 x y) (in custom lambda at level 1, left associativity). +Notation "x ∙ y" := (app2 x y) (in custom lambda at level 1, left associativity). Notation "'λ' t , x" := - (abs t x) (in custom lambda at level 90, + (abs1 t x) (in custom lambda at level 90, t custom lambda at level 99, x custom lambda at level 99, left associativity). +Notation "'λ' , x" := + (abs2 x) (in custom lambda at level 90, + x custom lambda at level 99, + left associativity). Coercion var : nat >-> term. -Reserved Notation "'[' x ':=' s ']' t" (in custom lambda at level 20). -Fixpoint substi (x : nat) (s t : term) : term := - match t with - | var y => if x =? y then s else var y - | free y => free y - | <{ m n }> => <{ ([x := s] m) ([x := s] n) }> - | <{ λ α, m }> => <{ λ α, [x := s] m }> - end - -where "'[' x ':=' s ']' t" := (substi x s t) (in custom lambda). - -Fixpoint β_reduce (m : term) : term := - match m with - | var x => var x - | free x => free x - | <{ (λ α , m) n }> => <{ [0 := n] m }> - | <{ m n }> => <{ {β_reduce m} {β_reduce n} }> - | <{ λ α, m }> => <{ λ α , {β_reduce m} }> - end. - -Fixpoint β_nf (m : term) : bool := - match m with - | var _ => true - | free _ => true - | <{ (λ α, m) n }> => false - | <{ m n }> => β_nf m && β_nf n - | <{ λ α, m }> => β_nf m - end. - -Reserved Notation "E ';' Γ '|-' t '::' T" - (at level 101, t custom lambda, T custom lambda at level 0). - Definition context := list type. Definition environment := list (nat * type). @@ -86,23 +73,114 @@ Proof. auto. Qed. +Reserved Notation "'[' x ':=' s ']' t" (in custom lambda at level 20). +Fixpoint substi (x : nat) (s t : term) : term := + match t with + | var y => if x =? y then s else var y + | free y => free y + | <{ m · n }> => <{ ([x := s] m) · ([x := s] n) }> + | <{ m ∙ n }> => <{ ([x := s] m) ∙ n }> + | <{ λ α, m }> => <{ λ α, [{x + 1} := s] m }> + | <{ λ , m }> => <{ λ , [x := s] m }> + end + +where "'[' x ':=' s ']' t" := (substi x s t) (in custom lambda). + +Reserved Notation "'[' x ':=' s ']ₐ' t" (in custom lambda at level 20). +Fixpoint ty_subst (x : nat) (s : type) (t : type) : type := + match t with + | tyvar n => if n =? x then s else tyvar n + | tyfree y => tyfree y + | <{ α -> β }> => <{ [ x := s ]ₐ α -> [ x := s ]ₐ β }> + | <{ Π α }> => <{ Π [ {x + 1} := s ]ₐ α }> + end + +where "'[' x ':=' s ']ₐ' t" := (ty_subst x s t) (in custom lambda). + +Reserved Notation "'[' x ':=' s ']ₜ' t" (in custom lambda at level 20). +Fixpoint substiₜ (x : nat) (s : type) (t : term) : term := + match t with + | var y => var y + | free y => free y + | <{ m · n }> => <{ ([ x := s ]ₜ m) · ([ x := s ]ₜ n) }> + | <{ m ∙ n }> => if type_eq_dec n (tyvar x) then + <{ m ∙ s }> + else <{ ([ x := s ]ₜ m) ∙ ([ x := s ]ₐ n) }> + | <{ λ α, m }> => <{ λ α, [ x := s ]ₜ m }> + | <{ λ , m }> => <{ λ , [ x := s ]ₜ m }> + end + +where "'[' x ':=' s ']ₜ' t" := (substiₜ x s t) (in custom lambda). + +Reserved Notation "E ';' Γ '|-' t '::' T" + (at level 101, t custom lambda, T custom lambda at level 0). + Inductive derivation : environment -> context -> term -> type -> Prop := | free_rule : forall E Γ x σ, lookup E x = Some σ -> E ; Γ |- {free x} :: σ | var_rule : forall E Γ x σ, nth_error Γ x = Some σ -> E ; Γ |- x :: σ -| app_rule : forall E Γ t1 t2 σ τ, +| app_rule1 : forall E Γ t1 t2 σ τ, (E ; Γ |- t1 :: (σ -> τ)) -> (E ; Γ |- t2 :: σ) -> - (E ; Γ |- t1 t2 :: τ) -| abs_rule : forall E Γ σ τ m, + (E ; Γ |- t1 · t2 :: τ) +| app_rule2 : forall E Γ m a b, + (E ; Γ |- m :: Π a) -> + (E ; Γ |- m ∙ b :: ([ 0 := b ]ₐ a)) +| abs_rule1 : forall E Γ σ τ m, (E ; σ :: Γ |- m :: τ) -> (E ; Γ |- λ σ, m :: (σ -> τ)) +| abs_rule2 : forall E Γ m a, + (E ; Γ |- m :: a) -> + (E ; Γ |- λ, m :: Π a) where "E ; Γ '|-' t '::' T" := (derivation E Γ t T). Hint Constructors derivation : core. +Section examples. + Let α := tyfree 0. + Let β := tyfree 1. + Let γ := tyfree 2. + + Example identity : + [] ; [] |- λ , (λ <0>, 0) :: Π <0> -> <0>. + Proof using Type. + auto. + Qed. + + Example identity_spec : + [] ; [] |- (λ , λ <0>, 0) ∙ α :: (α -> α). + Proof using Type. + apply app_rule2 with (a := <{<0> -> <0>}>). + exact identity. + Qed. + + Example comp : + [] ; [] |- λ , λ , λ , λ <2> -> <1>, λ <1> -> <0>, λ <2>, 1 · (2 · 0) + :: Π Π Π (<2> -> <1>) -> (<1> -> <0>) -> <2> -> <0>. + Proof using Type. + repeat econstructor. + Qed. + + Example comp_spec : + [] ; [] |- ((λ , λ , λ , λ <2> -> <1>, λ <1> -> <0>, λ <2>, 1 · (2 · 0)) ∙ α ∙ β ∙ γ) + :: ((α -> β) -> (β -> γ) -> α -> γ). + Proof using Type. + apply app_rule2 with (a := <{(α -> β) -> (β -> <0>) -> α -> <0>}>). + apply app_rule2 with (a := <{Π (α -> <1>) -> (<1> -> <0>) -> α -> <0>}>). + apply app_rule2 with (a := <{Π Π (<2> -> <1>) -> (<1> -> <0>) -> <2> -> <0>}>). + repeat econstructor. + Qed. + + Example book : + [] ; [] |- λ , λ <0> -> <0>, λ <0>, 1 · (1 · 0) :: Π (<0> -> <0>) -> <0> -> <0>. + Proof using Type. + repeat econstructor. + Qed. + +End examples. + Theorem uniqueness_of_types : forall E Γ t σ τ, E ; Γ |- t :: σ -> E ; Γ |- t :: τ -> σ = τ. Proof. @@ -113,23 +191,33 @@ Proof. - apply (IHt1 Γ <{σ0 -> σ}> <{σ1 -> τ}> H5) in H12. inversion H12. reflexivity. + - assert (G : pi a = pi a0) ; eauto. + inversion G. + reflexivity. - assert (G : τ0 = τ1) ; eauto. subst. reflexivity. + - apply (f_equal pi). + eauto. Qed. Fixpoint find_type (E : environment) (Γ : context) (m : term) : option type := match m with | var x => nth_error Γ x | free x => lookup E x - | app t1 t2 => match find_type E Γ t1, find_type E Γ t2 with - | Some (<{ σ -> τ }>), Some σ' => - if type_eq_dec σ σ' - then Some τ - else None - | _, _ => None - end - | abs σ t => option_map (arrow σ) (find_type E (σ :: Γ) t) + | app1 t1 t2 => match find_type E Γ t1, find_type E Γ t2 with + | Some (<{ σ -> τ }>), Some σ' => + if type_eq_dec σ σ' + then Some τ + else None + | _, _ => None + end + | app2 t σ => match find_type E Γ t with + | Some (pi τ) => Some <{[ 0 := σ ]ₐ τ}> + | _ => None + end + | abs1 σ t => option_map (arrow σ) (find_type E (σ :: Γ) t) + | abs2 t => option_map pi (find_type E Γ t) end. Theorem find_type_correct : forall E Γ t σ, @@ -146,123 +234,497 @@ Proof. destruct (type_eq_dec t0_1 t0); inversion H. subst. eauto. + - intros. + simpl in H. + destruct (find_type E Γ t0) eqn:Heq; simpl in H; inversion H ; eauto. + destruct t2; inversion H; auto. - intros. simpl in H. destruct (find_type E (t0 :: Γ) t1) eqn:Heq; inversion H. auto. + - intros. + simpl in H. + destruct (find_type E Γ t0) eqn:Heq; inversion H. + auto. Qed. -(* Fixpoint reverse_lookup_env (E : environment) (σ : type) : option nat := *) -(* match E with *) -(* | [] => None *) -(* | (x, σ') :: rest => *) -(* if type_eq_dec σ σ' then Some x else reverse_lookup_env rest σ *) -(* end. *) +Definition legal (t : term) := exists E Γ σ, E ; Γ |- t :: σ. -(* Definition env_no_dup (E : environment) := forall x σ σ', *) -(* In (x, σ) E -> In (x, σ') E -> σ = σ'. *) +Lemma no_self_referential_types : forall σ τ, + σ <> <{ σ -> τ }>. +Proof. + induction σ; intros τ contra; inversion contra. + apply (IHσ1 σ2). + assumption. +Qed. -(* Lemma reverse_lookup_env_correct : forall E x σ, *) -(* env_no_dup E -> reverse_lookup_env E σ = Some x -> lookup E x = Some σ. *) -(* Proof. *) -(* induction E. *) -(* - simpl. *) -(* discriminate. *) -(* - intros. *) -(* destruct a as [y τ]. *) -(* simpl in *. *) -(* destruct (eq_dec x y). *) -(* + rewrite e. *) -(* rewrite eqb_refl. *) -(* unfold env_no_dup in H. *) -(* specialize H with (x := y) (σ := σ) (σ' := τ) as H'. *) -(* apply (f_equal Some). *) -(* symmetry. *) -(* apply H'; try (simpl; left; subst; reflexivity). *) -(* destruct (type_eq_dec σ τ). *) -(* { simpl. left. rewrite e0. reflexivity. } *) +Theorem no_self_application : forall t, + ~ (legal <{t · t}>). +Proof. + intros t [E [Γ [σ H]]]. + inversion H. + subst. + assert (G : <{ σ0 -> σ }> = σ0). + { apply uniqueness_of_types with (E := E) (Γ := Γ) (t := t); assumption. } + symmetry in G. + exact (no_self_referential_types σ0 σ G). +Qed. + +Fixpoint β_reduce (m : term) : term := + match m with + | var x => var x + | free x => free x + | <{ (λ α , m) · n }> => <{ [0 := n] m }> + | <{ m · n }> => <{ {β_reduce m} · {β_reduce n} }> + | <{ λ α, m }> => <{ λ α , {β_reduce m} }> + | <{ (λ , m) ∙ n }> => <{ [0 := n]ₜ m }> + | <{ m ∙ n }> => <{ {β_reduce m} ∙ n }> + | <{ λ , m }> => <{ λ, {β_reduce m} }> + end. + +Reserved Notation "t1 '→β' t2" (at level 50). +Inductive β_reduce_r : term -> term -> Prop := +| var_β : forall x, var x →β var x +| free_β : forall x, free x →β free x +| redex1_β : forall α m n, <{ (λ α, m) · n }> →β <{ [0 := n] m }> +| redex2_β : forall m n, <{ (λ , m) ∙ n }> →β <{ [0 := n]ₜ m }> +| app1_compat_β_l : forall m n m', m →β m' -> <{ m · n }> →β <{ m' · n }> +| app1_compat_β_r : forall m n n', n →β n' -> <{ m · n }> →β <{ m · n' }> +| app2_compat_β : forall m n m', m →β m' -> <{ m ∙ n }> →β <{ m' ∙ n }> +| abs1_compat_β : forall α m m', m →β m' -> <{ λ α, m }> →β <{ λ α, m' }> +| abs2_compat_β : forall m m', m →β m' -> <{ λ , m }> →β <{ λ , m' }> + +where "t1 '→β' t2" := (β_reduce_r t1 t2). + +Definition β_reduce_r_ext := clos_refl_sym_trans term β_reduce_r. + +Notation "t1 '↠β' t2" := (β_reduce_r_ext t1 t2) (at level 50). + +(* Section church_rosser. *) + +(* Reserved Notation "t1 '↠' t2" (at level 50). *) +(* Inductive helper_relation : term -> term -> Prop := *) +(* | sym_h : forall t, t ↠ t *) +(* | abs1_compat_h : forall α m m', m ↠ m' -> <{ λ α, m }> ↠ <{ λ α, m' }> *) +(* | abs2_compat_h : forall m m', m ↠ m' -> <{ λ , m }> ↠ <{ λ , m' }> *) +(* | app1_compat_h : forall m m' n n', m ↠ m' -> n ↠ n' -> <{ m · n }> ↠ <{ m' · n' }> *) +(* | app2_compat_h : forall m m' n, m ↠ m' -> <{ m ∙ n }> ↠ <{ m' ∙ n }> *) +(* | redex1_h : forall α m n, <{ (λ α, m) · n }> ↠ <{ [0 := n] m }> *) +(* | redex2_h : forall m n, <{ (λ , m) ∙ n }> ↠ <{ [0 := n]ₜ m }> *) + +(* where "t1 '↠' t2" := (helper_relation t1 t2). *) + +(* Lemma substitution_lemma : forall M N L x y, *) +(* x < y -> *) +(* <{[y := L] ([x := N] M)}> = <{[x := [y := L] N] ([{y + 1} := L] M)}>. *) +(* Proof. *) +(* induction M ; auto. *) +(* - intros N L x y H. *) (* simpl. *) -(* right. *) -(* apply lookup_in. *) -(* apply IHE. *) -(* * unfold env_no_dup. *) -(* intros. *) -(* apply H with (x := x0); simpl; right; assumption. *) -(* * subst. *) -(* assumption. *) -(* + apply eqb_neq in n as n'. *) -(* rewrite n'. *) -(* apply IHE. *) -(* * unfold env_no_dup. *) -(* intros. *) -(* apply H with (x := x0); simpl; right; assumption. *) -(* * destruct (type_eq_dec σ τ). *) -(* { inversion H0. symmetry in H2. contradiction. } *) -(* assumption. *) -(* Qed. *) +(* destruct (x =? n) eqn:Heq. *) +(* + rewrite eqb_eq in Heq. *) +(* subst. *) +(* destruct (y =? n) eqn:Heq2. *) +(* { rewrite eqb_eq in Heq2. symmetry in Heq2. apply lt_neq in H. contradiction. } *) +(* apply lt_lt_add_r with (p := 1) in H. *) +(* apply lt_neq in H. *) +(* apply eqb_neq in H. *) +(* rewrite eqb_sym in H. *) +(* rewrite H. *) +(* simpl. *) +(* rewrite eqb_refl. *) +(* reflexivity. *) +(* + destruct (y =? n) eqn:Heq2. *) +(* * simpl. *) +(* rewrite Heq2. *) -(* Fixpoint reverse_lookup_context (Γ : context) (σ : type) : option nat := *) -(* match Γ with *) -(* | [] => None *) -(* | σ' :: rest => if type_eq_dec σ σ' *) -(* then Some 0 *) -(* else option_map S (reverse_lookup_context rest σ) *) -(* end. *) +(* * simpl. *) +(* rewrite Heq2. *) +(* rewrite Heq. *) +(* reflexivity. *) +(* - intros n p x y H1 H2. *) +(* simpl. *) +(* rewrite IHm1 ; auto. *) +(* rewrite IHm2 ; auto. *) +(* - intros n p x y H1 H2. *) +(* simpl. *) +(* rewrite IHm ; auto. *) +(* - intros n p x y H1 H2. *) +(* simpl. *) +(* rewrite IHm. *) +(* + Abort. *) -(* Lemma reverse_lookup_context_correct : forall Γ n σ, *) -(* reverse_lookup_context Γ σ = Some n -> nth_error Γ n = Some σ. *) -(* Proof. *) -(* induction Γ. *) -(* - intros. *) -(* inversion H. *) -(* - intros. *) -(* induction n. *) -(* + simpl in *. *) -(* destruct (type_eq_dec σ a). *) -(* { rewrite e; reflexivity. } *) -(* destruct (reverse_lookup_context Γ σ); inversion H. *) -(* + simpl. *) -(* apply IHΓ. *) -(* simpl in H. *) -(* destruct (type_eq_dec σ a) ; inversion H. *) -(* clear H1. *) -(* destruct (reverse_lookup_context Γ σ) ; inversion H. *) -(* reflexivity. *) -(* Qed. *) +(* Lemma reduct_in_subst : forall m n n' x, *) +(* n ↠ n' -> <{ [x := n] m }> ↠ <{ [x := n'] m }>. *) +(* Proof. *) +(* induction m ; try (intros; simpl; constructor; auto). *) +(* intros ℓ ℓ' x H. *) +(* simpl. *) +(* destruct (x =? n) ; auto using helper_relation. *) +(* Qed. *) -(* Definition or_else {A} (x1 x2 : option A) : option A := *) -(* match x1, x2 with *) -(* | Some x, _ => Some x *) -(* | _, Some x => Some x *) -(* | _, _ => None *) -(* end. *) +(* Lemma subst_reduct : forall m m' n n' x, *) +(* m ↠ m' -> n ↠ n' -> <{ [x := n] m }> ↠ <{ [x := n'] m' }>. *) +(* intros m m' n n' x H. *) +(* generalize dependent n. *) +(* generalize dependent n'. *) +(* generalize dependent x. *) +(* induction H ; try (intros; simpl; auto using helper_relation; fail). *) +(* - intros x n' n H. *) +(* apply reduct_in_subst. *) +(* assumption. *) +(* - intros x p q H. *) +(* simpl. *) +(* (* | redex1_h : forall α m n, <{ (λ α, m) · n }> ↠ <{ [0 := n] m }> *) *) +(* assert (G : <{ (λ α, [{x + 1} := q] m) · ([x := q] n) }> *) +(* ↠ <{ [0 := [x := q] n] ([{x + 1} := q] m) }>). *) +(* { apply redex1_h. } *) -(* Hint Unfold or_else : core. *) +(* Lemma abs1_char : forall α m n, *) +(* <{ λ α, m }> ↠ n -> exists m', n = <{ λ α, m' }> /\ m ↠ m'. *) +(* Proof. *) +(* intros α m n H1. *) +(* inversion H1; subst. *) +(* - exists m. *) +(* split; auto. *) +(* constructor. *) +(* - exists m'. *) +(* split; auto. *) +(* Qed. *) -(* Fixpoint find_term (E : environment) (Γ : context) (σ : type) : option term := *) -(* match σ with *) -(* | tyvar n => (or_else (option_map var (reverse_lookup_context Γ σ)) *) -(* (option_map free (reverse_lookup_env E σ))) *) -(* | arrow σ1 σ2 => option_map (abs σ1) (find_term E (σ1 :: Γ) σ2) *) -(* end. *) +(* Lemma abs2_char : forall m m', *) +(* <{ λ, m }> ↠ m' -> exists n, m' = <{λ, n}> /\ m ↠ n. *) +(* Proof. *) +(* intros m m' H. *) +(* inversion H; subst. *) +(* - exists m. *) +(* split; auto; try constructor. *) +(* - exists m'0. *) +(* split; auto; try constructor. *) +(* Qed. *) -(* Theorem find_term_correct : forall E Γ t σ, *) -(* env_no_dup E -> *) -(* find_term E Γ σ = Some t -> *) -(* E ; Γ |- t :: σ. *) -(* Proof. *) -(* intros. *) -(* generalize dependent Γ. *) -(* generalize dependent t0. *) -(* induction σ. *) -(* - intros t Γ H1. *) -(* simpl in *. *) -(* destruct (reverse_lookup_context Γ (tyvar n)) eqn:Hcon; *) -(* destruct (reverse_lookup_env E (tyvar n)) eqn:Henv; *) -(* simpl in H1; inversion H1; subst; *) -(* auto using reverse_lookup_context_correct; *) -(* auto using reverse_lookup_env_correct. *) -(* - intros t Γ H1. *) -(* simpl in H1. *) -(* destruct (find_term E (σ1 :: Γ) σ2) eqn:Heq; inversion H1; auto. *) -(* Qed. *) +(* Lemma app1_char : forall m n l, *) +(* <{ m · n }> ↠ l *) +(* -> (exists m' n', l = <{ m' · n' }> /\ m ↠ m' /\ n ↠ n') \/ *) +(* (exists α p, m = <{ λ α, p }> /\ l = <{[0 := n] p}>). *) +(* Proof. *) +(* intros m n l H. *) +(* inversion H ; subst ; auto. *) +(* - left. *) +(* exists m, n. *) +(* split ; auto. *) +(* split ; constructor. *) +(* - left. *) +(* exists m', n'. *) +(* auto. *) +(* - right. *) +(* exists α, m0. *) +(* auto. *) +(* Qed. *) + +(* Lemma helper_diamond : forall m m1 m2, *) +(* m ↠ m1 -> m ↠ m2 -> exists n, m1 ↠ n /\ m2 ↠ n. *) +(* Proof. *) +(* intros m m1 m2 H1. *) +(* generalize dependent m2. *) +(* induction H1. *) +(* - intros m2 H2. *) +(* exists m2. *) +(* split ; try constructor; auto. *) +(* - intros m2 H2. *) +(* apply abs1_char in H2 as [t [G1 G2]]. *) +(* subst. *) +(* apply (IHhelper_relation t) in G2 as [n [F1 F2]]. *) +(* exists <{λ α, n}>. *) +(* split; constructor; assumption. *) +(* - intros m2 H2. *) +(* apply abs2_char in H2 as [n [G1 G2]]. *) +(* subst. *) +(* apply (IHhelper_relation n) in G2 as [n' [F1 F2]]. *) +(* exists <{λ, n'}>. *) +(* split; constructor; assumption. *) +(* - intros m2 H2. *) +(* apply app1_char in H2 as [[p [q [G1 [G2 G3]]]] | H2]; subst. *) +(* + apply IHhelper_relation1 in G2 as [p' [Hp1 Hp2]]. *) +(* apply IHhelper_relation2 in G3 as [q' [Hq1 Hq2]]. *) +(* exists <{p' · q'}>. *) +(* split; auto using helper_relation. *) +(* + destruct H2 as [α [p [G1 G2]]]. *) +(* subst. *) +(* apply abs1_char in H1_ as [l [Hm Hl]]. *) +(* subst. *) +(* exists <{[0 := n'] l}>. *) +(* split. *) +(* * constructor. *) +(* * *) +(* (* apply IHhelper_relation1 in H1_. *) *) +(* (* apply IHhelper_relation2 in H1_0. *) *) + +(* End church_rosser. *) + +Reserved Notation "t1 ≡ t2" (at level 50). +Inductive β_equiv : term -> term -> Prop := +| reduce : forall t1 t2, β_reduce t1 = t2 -> t1 ≡ t2 +| refl_β : forall t, t ≡ t +| sym_β : forall t1 t2, t1 ≡ t2 -> t2 ≡ t1 +| trans_β : forall t1 t2 t3, + t1 ≡ t2 -> t2 ≡ t3 -> t1 ≡ t3 + +where "t1 ≡ t2" := (β_equiv t1 t2). + +Hint Constructors β_equiv : core. + +Instance β_equiv_equiv : Equivalence β_equiv. +Proof. + constructor; eauto. +Qed. + +(* Proving these requires proving CR *) +Instance β_equiv_app1_l {t : term} : Proper (β_equiv ==> β_equiv) (fun s => app1 s t). +Proof. +Abort. + +Instance β_equiv_app2 {σ : type} : Proper (β_equiv ==> β_equiv) (fun t => app2 t σ). +Proof. +Abort. + +Instance β_equiv_abs2 : Proper (β_equiv ==> β_equiv) abs2. +Proof. + intros x y H. + induction H; auto. + - constructor. + simpl. + rewrite H. + reflexivity. + - rewrite IHβ_equiv1. + rewrite IHβ_equiv2. + reflexivity. +Qed. + +Example test t1 t2 : t1 ≡ t2 -> abs2 t1 ≡ abs2 t2. +Proof. + intros H. + rewrite H. + reflexivity. +Qed. + +Ltac simple_compute := + repeat (eapply trans_β; + try (apply reduce; reflexivity)). + +Section book_examples. + Let α := tyfree 0. + Let β := tyfree 1. + Let γ := tyfree 2. + + Example ex3_2 : + [] ; [] |- λ , λ , λ , λ <2> -> <1>, λ <1> -> <0>, λ <2>, 1 · (2 · 0) + :: Π Π Π (<2> -> <1>) -> (<1> -> <0>) -> <2> -> <0>. + Proof using Type. + repeat econstructor. + Qed. + + Let nat' := tyfree 3. + Let bool' := tyfree 4. + Example ex3_4 : + [] ; [] |- (λ , λ , λ <1> -> <1>, λ <1> -> <0>, λ <1>, 1 · (2 · (2 · 0))) ∙ nat' ∙ bool' + :: ((nat' -> nat') -> (nat' -> bool') -> nat' -> bool'). + Proof using Type. + apply app_rule2 with (a := <{(nat' -> nat') -> (nat' -> <0>) -> nat' -> <0>}>). + apply app_rule2 with (a := <{Π (<1> -> <1>) -> (<1> -> <0>) -> <1> -> <0>}>). + repeat econstructor. + Qed. + + Example ex3_5 : forall σ, + [(0, <{Π <0>}>)] ; [] |- {free 0} ∙ σ :: σ. + Proof using Type. + intros. + apply app_rule2 with (a := <{<0>}>). + auto. + Qed. + + Example ex3_6a : [] ; [] |- + λ , λ , λ nat' -> <1>, λ <1> -> nat' -> <0> , λ nat', 1 · (2 · 0) · 0 :: + Π Π (nat' -> <1>) -> (<1> -> nat' -> <0>) -> nat' -> <0>. + Proof using Type. + repeat econstructor. + Qed. + + Example ex3_6b : [] ; [] |- + λ, λ ((α -> γ) -> <0>), λ (α -> β), λ (β -> γ), + 2 · (λ α, 1 · (2 · 0)) :: + Π ((α -> γ) -> <0>) -> (α -> β) -> (β -> γ) -> <0>. + Proof using Type. + repeat econstructor. + Qed. +End book_examples. + +Section numbers_bools. + Definition nat' := <{Π (<0> -> <0>) -> <0> -> <0>}>. + Definition zero := <{λ , λ <0> -> <0>, λ <0>, 0}>. + Definition one := <{λ , λ <0> -> <0>, λ <0>, 1 · 0}>. + Definition two := <{λ , λ <0> -> <0>, λ <0>, 1 · (1 · 0)}>. + + Definition succ := <{λ {nat'}, λ , λ <0> -> <0>, λ <0>, 1 · (2 ∙ <0> · 1 · 0)}>. + Definition add := <{λ {nat'}, λ {nat'}, λ , λ <0> -> <0>, λ <0>, + 3 ∙ <0> · 1 · (2 ∙ <0> · 1 · 0) + }>. + + Example zero_nat : [] ; [] |- zero :: nat'. + Proof using Type. + repeat econstructor. + Qed. + + Example succ_nat_nat : [] ; [] |- succ :: (nat' -> nat'). + Proof using Type. + unfold nat'. + repeat econstructor. + apply app_rule2 with (a := <{(<0> -> <0>) -> <0> -> <0>}>). + repeat econstructor. + Qed. + + Example succ_zero_one : app1 succ zero ≡ one. + Proof using Type. + simple_compute. + Qed. + + Example succ_one_two : app1 succ one ≡ two. + Proof using Type. + simple_compute. + Qed. + + Example one_p_one_two : <{{add} · {one} · {one}}> ≡ two. + Proof using Type. + simple_compute. + Qed. + + Definition bool' := <{Π <0> -> <0> -> <0>}>. + Definition true := <{λ , λ <0>, λ <0>, 1}>. + Definition false := <{λ , λ <0>, λ <0>, 0}>. + Definition neg := <{λ {bool'}, λ , (0 ∙ <0>) · ({false} ∙ <0>) · ((true) ∙ <0>)}>. + + Example neg_true_false : app1 neg true ≡ false. + Proof using Type. + simple_compute. + Qed. + + Example neg_false_true : app1 neg false ≡ true. + Proof using Type. + simple_compute. + Qed. + + Definition M := <{ + λ {bool'}, λ {bool'}, λ , λ <0>, λ <0>, + 3 ∙ <0> · (2 ∙ <0> · 1 · 0) · (2 ∙ <0> · 0 · 0) + }>. + + (* M is and *) + Example M_true_true : <{{M} · {true} · {true}}> ≡ true. + Proof using Type. + simple_compute. + Qed. + + Example M_true_false : <{{M} · {true} · {false}}> ≡ false. + Proof using Type. + simple_compute. + Qed. + + Example M_false_true : <{{M} · {false} · {true}}> ≡ false. + Proof using Type. + simple_compute. + Qed. + + Example M_false_false : <{{M} · {false} · {false}}> ≡ false. + Proof using Type. + simple_compute. + Qed. + + Definition or := <{ + λ {bool'}, λ {bool'}, + 1 ∙ {bool'} · {true} · 0 + }>. + + Example or_true_true : <{{or} · {true} · {true}}> ≡ true. + Proof using Type. + simple_compute. + Qed. + + Example or_true_false : <{{or} · {true} · {false}}> ≡ true. + Proof using Type. + simple_compute. + Qed. + + Example or_false_true : <{{or} · {false} · {true}}> ≡ true. + Proof using Type. + simple_compute. + Qed. + + Example or_false_false : <{{or} · {false} · {false}}> ≡ false. + Proof using Type. + simple_compute. + Qed. + + Definition xor := <{ + λ {bool'}, λ {bool'}, 1 ∙ {bool'} · ({neg} · 0) · 0 + }>. + + Example xor_true_true : <{{xor} · {true} · {true}}> ≡ false. + Proof using Type. + simple_compute. + Qed. + + Example xor_true_false : <{{xor} · {true} · {false}}> ≡ true. + Proof using Type. + simple_compute. + Qed. + + Example xor_false_true : <{{xor} · {false} · {true}}> ≡ true. + Proof using Type. + simple_compute. + Qed. + + Example xor_false_false : <{{xor} · {false} · {false}}> ≡ false. + Proof using Type. + simple_compute. + Qed. + + Definition impl := <{ + λ {bool'}, λ {bool'}, + 1 ∙ {bool'} · 0 · {true} + }>. + + Example impl_true_true : <{{impl} · {true} · {true}}> ≡ true. + Proof using Type. + simple_compute. + Qed. + + Example impl_true_false : <{{impl} · {true} · {false}}> ≡ false. + Proof using Type. + simple_compute. + Qed. + + Example impl_false_true : <{{impl} · {false} · {true}}> ≡ true. + Proof using Type. + simple_compute. + Qed. + + Example impl_false_false : <{{impl} · {false} · {false}}> ≡ true. + Proof using Type. + simple_compute. + Qed. + + Definition is_zero := <{ + λ {nat'}, 0 ∙ {bool'} · (λ {bool'}, {false}) · {true} + }>. + + Example zero_is_zero : app1 is_zero zero ≡ true. + Proof using Type. + simple_compute. + Qed. + + Example one_not_zero : app1 is_zero one ≡ false. + Proof using Type. + simple_compute. + Qed. + +End numbers_bools.