-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathlist.v
128 lines (111 loc) · 2.22 KB
/
list.v
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
#[global]
Set Primitive Projections.
#[global]
Unset Printing Primitive Projection Parameters.
#[global]
Set Universe Polymorphism.
#[global]
Set Default Goal Selector "!".
Require Import Coq.Unicode.Utf8.
Require Import Coq.Program.Tactics.
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import Psatz.
Import IfNotations.
Import ListNotations.
Definition Π y: list Type → Type :=
fix loop l :=
match l with
| [] => unit
| H :: T => prod (y H) (loop T)
end.
Definition Mor (A B: list Type) :=
∀ x, Π (λ a, x → a) A → Π (λ b, x → b) B.
Definition map {A B} (f: A → B): Mor [A] [B].
Proof.
intros ? [H ?].
apply (λ x, f (H x), tt).
Defined.
Definition fst: ∀ {A B}, Mor (A ++ B) A.
Proof.
intros A B.
intros ? X.
induction A.
all: cbn in *.
- apply tt.
- destruct X as [H T].
split.
+ apply H.
+ apply IHA.
apply T.
Defined.
Definition snd: ∀ {A B}, Mor (A ++ B) B.
Proof.
intros A.
induction A.
- intros ? ? X.
cbn.
apply X.
- intros ? ? [H T].
cbn in *.
apply IHA.
auto.
Defined.
Definition fanout:
∀ A B C,
Mor C A → Mor C B → Mor C (A ++ B).
Proof.
intro A.
induction A.
all: cbn in *.
- intros ? ? ? g.
apply g.
- intros ? ? f g ? X.
cbn.
split.
+ apply f.
cbn in *.
auto.
+ refine (IHA _ _ _ g _ _).
* intros ? ?.
apply f.
cbn.
auto.
* apply X.
Defined.
Definition entail A B := ∀ x, Π (λ a, x → a) A → (x → B).
Infix "⊢" := entail (at level 90).
Definition index: ∀ {A} (Γ: list A) n, (n < length Γ) → A.
Proof.
intros ? Γ n.
induction n.
- intros p.
destruct Γ as [|H T].
1: cbn in *; Psatz.lia.
apply H.
- intro.
apply IHn.
Psatz.lia.
Defined.
Definition var {Γ} n p: Γ ⊢ index Γ n p.
Proof.
induction n.
- destruct Γ.
1: cbn in *;Psatz.lia.
intros ? [H ?] ?.
apply H.
auto.
- intros ? H x.
apply (IHn _ _ H x).
Defined.
Definition curry {A B Γ} (f: (A :: Γ) ⊢ B): Γ ⊢ (A → B).
Proof.
intros T X t a.
apply (f T (λ _, a, X) t).
Defined.
#[program]
Definition foo {Γ A}: A :: Γ ⊢ A := var 0 _.
Next Obligation.
Proof.
Psatz.lia.
Qed.