730 lines
22 KiB
Coq
730 lines
22 KiB
Coq
Require Import PeanoNat.
|
||
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
|
||
| tyfree : nat -> type
|
||
| arrow : type -> type -> type
|
||
| pi : type -> type.
|
||
|
||
Scheme Equality for type.
|
||
|
||
Inductive term : Set :=
|
||
| var : nat -> term
|
||
| free : nat -> 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 "'Π' 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" :=
|
||
(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.
|
||
|
||
Definition context := list type.
|
||
Definition environment := list (nat * type).
|
||
|
||
Fixpoint lookup (E : environment) (x : nat) : option type :=
|
||
match E with
|
||
| [] => None
|
||
| (x', σ) :: rest => if x =? x' then Some σ else lookup rest x
|
||
end.
|
||
|
||
Lemma lookup_in : forall E x σ,
|
||
lookup E x = Some σ -> In (x, σ) E.
|
||
Proof.
|
||
induction E.
|
||
- simpl; discriminate.
|
||
- intros.
|
||
destruct a as [y τ].
|
||
simpl in H.
|
||
destruct (x =? y) eqn:Heq.
|
||
{ apply eqb_eq in Heq; subst; inversion H; simpl; left; reflexivity. }
|
||
simpl.
|
||
right.
|
||
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_rule1 : forall E Γ t1 t2 σ τ,
|
||
(E ; Γ |- t1 :: (σ -> τ)) ->
|
||
(E ; Γ |- t2 :: σ) ->
|
||
(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.
|
||
intros E Γ t.
|
||
generalize dependent Γ.
|
||
induction t; intros; inversion H; inversion H0; subst;
|
||
try (rewrite H4 in H9; inversion H9; reflexivity).
|
||
- 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
|
||
| 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 σ,
|
||
find_type E Γ t = Some σ -> E ; Γ |- t :: σ.
|
||
Proof.
|
||
intros E Γ t.
|
||
generalize dependent Γ.
|
||
induction t ; auto.
|
||
- intros.
|
||
simpl in H.
|
||
destruct (find_type E Γ t1) eqn:Heq ; inversion H.
|
||
destruct t0 ; inversion H.
|
||
destruct (find_type E Γ t2) eqn:Heq2; inversion H.
|
||
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.
|
||
|
||
Definition legal (t : term) := exists E Γ σ, E ; Γ |- t :: σ.
|
||
|
||
Lemma no_self_referential_types : forall σ τ,
|
||
σ <> <{ σ -> τ }>.
|
||
Proof.
|
||
induction σ; intros τ contra; inversion contra.
|
||
apply (IHσ1 σ2).
|
||
assumption.
|
||
Qed.
|
||
|
||
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. *)
|
||
(* 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. *)
|
||
|
||
(* * 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 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. *)
|
||
|
||
(* 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. } *)
|
||
|
||
(* 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. *)
|
||
|
||
(* 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. *)
|
||
|
||
(* 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.
|