1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
|
Require Import Coq.Program.Program Coq.Program.Equations.
Variable A : Set.
Inductive vector : nat -> Type := vnil : vector 0 | vcons : A -> forall {n}, vector n -> vector (S n).
Goal forall n, forall v : vector (S n), vector n.
Proof.
intros n H.
dependent destruction H.
assumption.
Save.
Require Import ProofIrrelevance.
Goal forall n, forall v : vector (S n), exists v' : vector n, exists a : A, v = vcons a v'.
Proof.
intros n v.
dependent destruction v.
exists v ; exists a.
reflexivity.
Save.
(* Extraction Unnamed_thm. *)
Inductive type : Type :=
| base : type
| arrow : type -> type -> type.
Notation " t --> t' " := (arrow t t') (at level 20, t' at next level).
Inductive ctx : Type :=
| empty : ctx
| snoc : ctx -> type -> ctx.
Bind Scope context_scope with ctx.
Delimit Scope context_scope with ctx.
Arguments Scope snoc [context_scope].
Notation " Γ , τ " := (snoc Γ τ) (at level 25, τ at next level, left associativity) : context_scope.
Fixpoint conc (Δ Γ : ctx) : ctx :=
match Δ with
| empty => Γ
| snoc Δ' x => snoc (conc Δ' Γ) x
end.
Notation " Γ ; Δ " := (conc Δ Γ) (at level 25, left associativity) : context_scope.
Reserved Notation " Γ ⊢ τ " (at level 30, no associativity).
Inductive term : ctx -> type -> Type :=
| ax : `(Γ, τ ⊢ τ)
| weak : `{Γ ⊢ τ -> Γ, τ' ⊢ τ}
| abs : `{Γ, τ ⊢ τ' -> Γ ⊢ τ --> τ'}
| app : `{Γ ⊢ τ --> τ' -> Γ ⊢ τ -> Γ ⊢ τ'}
where " Γ ⊢ τ " := (term Γ τ) : type_scope.
Hint Constructors term : lambda.
Open Local Scope context_scope.
Ltac eqns := subst ; reverse ; simplify_dep_elim ; simplify_IH_hyps.
Lemma weakening : forall Γ Δ τ, Γ ; Δ ⊢ τ ->
forall τ', Γ , τ' ; Δ ⊢ τ.
Proof with simpl in * ; eqns ; eauto with lambda.
intros Γ Δ τ H.
dependent induction H.
destruct Δ as [|Δ τ'']...
destruct Δ as [|Δ τ'']...
destruct Δ as [|Δ τ'']...
apply abs.
specialize (IHterm Γ (Δ, τ'', τ0) τ'0)...
intro. eapply app...
Defined.
Lemma exchange : forall Γ Δ α β τ, term (Γ, α, β ; Δ) τ -> term (Γ, β, α ; Δ) τ.
Proof with simpl in * ; eqns ; eauto.
intros until 1.
dependent induction H.
destruct Δ ; eqns.
apply weak ; apply ax.
apply ax.
destruct Δ...
pose (weakening Γ (empty, α))...
apply weak...
apply abs...
specialize (IHterm Γ (Δ, τ0))...
eapply app...
Defined.
(** Example by Andrew Kenedy, uses simplification of the first component of dependent pairs. *)
Set Implicit Arguments.
Inductive Ty :=
| Nat : Ty
| Prod : Ty -> Ty -> Ty.
Inductive Exp : Ty -> Type :=
| Const : nat -> Exp Nat
| Pair : forall t1 t2, Exp t1 -> Exp t2 -> Exp (Prod t1 t2)
| Fst : forall t1 t2, Exp (Prod t1 t2) -> Exp t1.
Inductive Ev : forall t, Exp t -> Exp t -> Prop :=
| EvConst : forall n, Ev (Const n) (Const n)
| EvPair : forall t1 t2 (e1:Exp t1) (e2:Exp t2) e1' e2',
Ev e1 e1' -> Ev e2 e2' -> Ev (Pair e1 e2) (Pair e1' e2')
| EvFst : forall t1 t2 (e:Exp (Prod t1 t2)) e1 e2,
Ev e (Pair e1 e2) ->
Ev (Fst e) e1.
Lemma EvFst_inversion : forall t1 t2 (e:Exp (Prod t1 t2)) e1, Ev (Fst e) e1 -> exists e2, Ev e (Pair e1 e2).
intros t1 t2 e e1 ev. dependent destruction ev. exists e3 ; assumption.
Qed.
|