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
|
Require Import Coq.Program.Program.
Set Implicit Arguments.
Unset Strict Implicit.
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.
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).
Inductive term : ctx -> type -> Type :=
| ax : forall Γ τ, term (Γ, τ) τ
| weak : forall Γ τ, term Γ τ -> forall τ', term (Γ, τ') τ
| abs : forall Γ τ τ', term (Γ , τ) τ' -> term Γ (τ --> τ')
| app : forall Γ τ τ', term Γ (τ --> τ') -> term Γ τ -> term Γ τ'.
Lemma weakening : forall Γ Δ τ, term (Γ ; Δ) τ ->
forall τ', term (Γ , τ' ; Δ) τ.
Proof with simpl in * ; auto ; simpl_depind.
intros Γ Δ τ H.
dependent induction H.
destruct Δ...
apply weak ; apply ax.
apply ax.
destruct Δ...
specialize (IHterm Γ empty)...
apply weak...
apply weak...
destruct Δ...
apply weak ; apply abs ; apply H.
apply abs...
specialize (IHterm Γ0 (Δ, t, τ))...
apply app with τ...
Qed.
Lemma exchange : forall Γ Δ α β τ, term (Γ, α, β ; Δ) τ -> term (Γ, β, α ; Δ) τ.
Proof with simpl in * ; simpl_depind ; 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 Γ0 α β (Δ, τ))...
eapply app with τ...
Save.
|
