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
|
Require Import Coq.Program.Program.
Set Manual Implicit Arguments.
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, t at next level, left associativity).
Fixpoint conc (Δ Γ : ctx) : ctx :=
match Δ with
| empty => Γ
| snoc Δ' x => snoc (conc Δ' Γ) x
end.
Notation " Γ ;; Δ " := (conc Δ Γ) (at level 25, left associativity) : context_scope.
Inductive term : ctx -> type -> Type :=
| ax : forall Γ τ, term (snoc Γ τ) τ
| weak : forall Γ τ, term Γ τ -> forall τ', term (Γ ,, τ') τ
| abs : forall Γ τ τ', term (snoc Γ τ) τ' -> term Γ (τ --> τ')
| app : forall Γ τ τ', term Γ (τ --> τ') -> term Γ τ -> term Γ τ'.
Hint Constructors term : lambda.
Open Local Scope context_scope.
Notation " Γ |-- τ " := (term Γ τ) (at level 0) : type_scope.
Lemma weakening : forall Γ Δ τ, term (Γ ;; Δ) τ ->
forall τ', term (Γ ,, τ' ;; Δ) τ.
Proof with simpl in * ; reverse ; simplify_dep_elim ; simplify_IH_hyps ; eauto with lambda.
intros Γ Δ τ H.
dependent induction H.
destruct Δ...
destruct Δ...
destruct Δ...
apply abs...
specialize (IHterm (Δ,, t,, τ)%ctx Γ0)...
intro.
apply app with τ...
Qed.
Lemma exchange : forall Γ Δ α β τ, term (Γ,, α,, β ;; Δ) τ -> term (Γ,, β,, α ;; Δ) τ.
Proof with simpl in * ; subst ; reverse ; simplify_dep_elim ; simplify_IH_hyps ; auto.
intros until 1.
dependent induction H.
destruct Δ...
apply weak ; apply ax.
apply ax.
destruct Δ...
pose (weakening Γ0 (empty,, α))...
apply weak...
apply abs...
specialize (IHterm (Δ ,, τ))...
eapply app with τ...
Save.
|
