Skip to content

Commit 8d46bc3

Browse files
NotBad4Ufblanqui
NotBad4U
and
fblanqui
authored
Add lemmas and definitions from Alethe development (#74)
- Bool: imp, xorb, not_inj and theorems on if-then-else - Epsilon: εₑ - List: foldl, foldr, All, mergesort and its correctness - Nat: parity, div2, shifts, bitwise operations and strong induction - Pos: theorems on multiplication - Prod: theorems on the Cartesian product - Coprod: the co-Cartesian product (disjoint sum) - Subset: subset types - DepProd: dependent products and transport - Z: theorems on multiplication, power and comparison --------- Co-authored-by: Frédéric Blanqui <frederic.blanqui@inria.fr>
1 parent d759a55 commit 8d46bc3

12 files changed

Lines changed: 1954 additions & 100 deletions

File tree

‎Bool.lp‎

Lines changed: 140 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -104,6 +104,26 @@ begin
104104
{ simplify; assume h0 h1; refine h1 }
105105
end;
106106

107+
opaque symbol notK b : π (not (not b) = b) ≔
108+
begin
109+
induction
110+
{ reflexivity }
111+
{ reflexivity }
112+
end;
113+
114+
opaque symbol not_inj [b c] : π (not b = not c) → π (b = c) ≔
115+
begin
116+
induction
117+
{ induction
118+
{ assume h; reflexivity }
119+
{ assume h; apply ⊥ₑ (false≠true h) }
120+
}
121+
{ induction
122+
{ assume h; apply ⊥ₑ (true≠false h) }
123+
{ assume h; reflexivity }
124+
}
125+
end;
126+
107127
// or
108128

109129
symbol or : 𝔹 → 𝔹 → 𝔹;
@@ -129,6 +149,49 @@ begin
129149
{reflexivity}
130150
end;
131151

152+
// imp
153+
154+
symbol imp (b c : 𝔹) : 𝔹 ≔ not b or c;
155+
156+
notation imp infix left 20;
157+
158+
opaque symbol ⇒_istrue [p q : 𝔹] : π(p imp q) → π(p ⇒ q) ≔
159+
begin
160+
induction
161+
{ induction
162+
{ assume h1; refine (λ x, x) }
163+
{ assume h1 h2; refine h1 }
164+
}
165+
{
166+
induction
167+
{ assume h1 h2; apply h1 }
168+
{ assume h1; refine (λ x, x) }
169+
}
170+
end;
171+
172+
opaque symbol istrue_imp [p q : 𝔹] : π(p ⇒ q) → π(p imp q) ≔
173+
begin
174+
induction
175+
{ induction
176+
{ assume h; apply ⊤ᵢ }
177+
{ assume h; apply h ⊤ᵢ }
178+
}
179+
{ induction
180+
{ assume h; apply ⊤ᵢ }
181+
{ assume h; apply ⊤ᵢ }
182+
}
183+
end;
184+
185+
opaque symbol impᵢ [p q : 𝔹] : (π p → π q) → π (p imp q) ≔
186+
begin
187+
assume p q h; apply @istrue_imp p q h;
188+
end;
189+
190+
opaque symbol impₑ [p q : 𝔹] : π (p imp q) → π p → π q ≔
191+
begin
192+
assume p q h; refine @⇒_istrue p q h;
193+
end;
194+
132195
opaque symbol ∨_istrue [p q : 𝔹] : π(p or q) → π(p ∨ q) ≔
133196
begin
134197
induction
@@ -226,9 +289,86 @@ begin
226289
{ assume q i; apply ⊥ₑ i; }
227290
end;
228291

292+
// xorb
293+
294+
symbol xorb : 𝔹 → 𝔹 → 𝔹;
295+
296+
notation xorb infix left 22;
297+
298+
rule false xorb $b ↪ $b
299+
with true xorb $b ↪ not $b;
300+
301+
opaque symbol xorbᵢ₁ [p q : 𝔹] : π p → π (not q) → π (p xorb q) ≔
302+
begin
303+
induction
304+
{ assume q h i; apply i }
305+
{ assume q h i; apply ⊥ₑ h }
306+
end;
307+
308+
opaque symbol xorbᵢ₂ [p q : 𝔹] : π (not p) → π q → π (p xorb q) ≔
309+
begin
310+
induction
311+
{ assume q h i; apply ⊥ₑ h }
312+
{ assume q h i; apply i }
313+
end;
314+
315+
opaque symbol xorbₑ [p q : 𝔹] (r : 𝔹) :
316+
π (p xorb q) → (π p → π (not q) → π r) → (π (not p) → π q → π r) → π r ≔
317+
begin
318+
induction
319+
{ assume q r h h1 h2; apply h1 ⊤ᵢ h }
320+
{ assume q r h h1 h2; apply h2 ⊤ᵢ h }
321+
end;
322+
229323
// if-then-else
230324

231325
symbol if : 𝔹 → Π [a], τ a → τ a → τ a;
232326

233327
rule if true $x _ ↪ $x
234328
with if false _ $y ↪ $y;
329+
330+
opaque symbol if_true [a] (x y : τ a) : π (if true x y = x) ≔
331+
begin reflexivity end;
332+
333+
opaque symbol if_false [a] (x y : τ a) : π (if false x y = y) ≔
334+
begin reflexivity end;
335+
336+
opaque symbol if_same b [a] (x : τ a) : π (if b x x = x) ≔
337+
begin
338+
assume b a x;
339+
refine ∨ₑ (case_𝔹 b) _ _
340+
{ assume h; rewrite h; reflexivity }
341+
{ assume h; rewrite h; reflexivity }
342+
end;
343+
344+
opaque symbol if_id b : π (if b true false = b) ≔
345+
begin
346+
induction
347+
{ reflexivity }
348+
{ reflexivity }
349+
end;
350+
351+
opaque symbol if_not b [a] (x y : τ a) : π (if (not b) x y = if b y x) ≔
352+
begin
353+
assume b a x y;
354+
refine ∨ₑ (case_𝔹 b) _ _
355+
{ assume h; rewrite h; reflexivity }
356+
{ assume h; rewrite h; reflexivity }
357+
end;
358+
359+
opaque symbol if_istrue [b : 𝔹] [a] (x y : τ a) : π b → π (if b x y = x) ≔
360+
begin
361+
assume b a x y h;
362+
refine ∨ₑ (case_𝔹 b) _ _
363+
{ assume h1; rewrite h1; reflexivity }
364+
{ assume h1; apply ⊥ₑ (false=¬istrue h1 h) }
365+
end;
366+
367+
opaque symbol if_isfalse [b : 𝔹] [a] (x y : τ a) : π (not b) → π (if b x y = y) ≔
368+
begin
369+
assume b a x y h;
370+
refine ∨ₑ (case_𝔹 b) _ _
371+
{ assume h1; apply ⊥ₑ (istrue_not h (true=istrue h1)) }
372+
{ assume h1; rewrite h1; reflexivity }
373+
end;
374+

‎CHANGES.md‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,16 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
1111
- Univ: universe levels for Set and Prop
1212
- Quotient: quotient types
1313
- NaryFun: n-ary functions and relations
14+
- Bool: imp, xorb, not_inj and theorems on if-then-else
15+
- Epsilon: εₑ
16+
- List: foldl, foldr, All, mergesort and its correctness
17+
- Nat: parity, div2, shifts, bitwise operations and strong induction
18+
- Pos: theorems on multiplication
19+
- Prod: theorems on the Cartesian product
20+
- Coprod: the co-Cartesian product (disjoint sum)
21+
- Subset: subset types
22+
- DepProd: dependent products and transport
23+
- Z: theorems on multiplication, power and comparison
1424

1525
### Changed
1626

‎Coprod.lp‎

Lines changed: 144 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,144 @@
1+
// Co-Cartesian product (disjoint sum)
2+
3+
require open Stdlib.FOL Stdlib.Eq;
4+
5+
(a: Set) (b: Set) inductive Sum: TYPE ≔
6+
| inl: τ a → Sum a b
7+
| inr: τ b → Sum a b;
8+
9+
constant symbol sum : Set → Set → Set;
10+
11+
rule τ (sum $a $b) ↪ Sum $a $b;
12+
13+
// Universal property: a map out of a sum is given by case analysis
14+
15+
symbol sum_case [a b c] : τ (sum a b) → (τ a → τ c) → (τ b → τ c) → τ c;
16+
17+
rule sum_case (inl $x) $f _ ↪ $f $x
18+
with sum_case (inr $y) _ $g ↪ $g $y;
19+
20+
opaque symbol sum_case_uniq [a b c] (h: τ (sum a b) → τ c) (s: τ (sum a b)) :
21+
π (sum_case s (λ x, h (inl x)) (λ y, h (inr y)) = h s) ≔
22+
begin
23+
assume a b c h; induction { reflexivity } { reflexivity }
24+
end;
25+
26+
opaque symbol η_sum [a b] (s: τ (sum a b)) :
27+
π (sum_case s (λ x, inl x) (λ y, inr y) = s) ≔
28+
begin
29+
assume a b; induction { reflexivity } { reflexivity }
30+
end;
31+
32+
// non confusion of constructors
33+
34+
symbol is_inl [a b] : τ (sum a b) → Prop;
35+
36+
rule is_inl (inl _) ↪ ⊤
37+
with is_inl (inr _) ↪ ⊥;
38+
39+
opaque symbol inr≠inl [a b] (x: τ a) (y: τ b) : π (@inr a b y ≠ inl x) ≔
40+
begin assume a b x y h; refine ind_eq h (λ s, is_inl s) ⊤ᵢ end;
41+
42+
opaque symbol inl≠inr [a b] (x: τ a) (y: τ b) : π (@inl a b x ≠ inr y) ≔
43+
begin assume a b x y h; apply inr≠inl x y; symmetry; apply h end;
44+
45+
symbol outl [a b] (s: τ (sum a b)) : τ a ≔ sum_case s (λ x, x) (λ _, el a);
46+
symbol outr [a b] (s: τ (sum a b)) : τ b ≔ sum_case s (λ _, el b) (λ y, y);
47+
48+
opaque symbol inl_inj [a b] (x x': τ a) : π (@inl a b x = inl x') → π (x = x') ≔
49+
begin assume a b x x' h; refine feq (λ s, @outl a b s) h end;
50+
51+
opaque symbol inr_inj [a b] (y y': τ b) : π (@inr a b y = inr y') → π (y = y') ≔
52+
begin assume a b y y' h; refine feq (λ s, @outr a b s) h end;
53+
54+
// induction principle with equalities
55+
56+
opaque symbol case_Sum [a b] (s: τ (sum a b)) :
57+
π ((`∃ x, s = inl x) ∨ (`∃ y, s = inr y)) ≔
58+
begin
59+
assume a b; induction
60+
{ assume x; apply ∨ᵢ₁; apply ∃ᵢ x; reflexivity }
61+
{ assume y; apply ∨ᵢ₂; apply ∃ᵢ y; reflexivity }
62+
end;
63+
64+
opaque symbol ind_Sum_eq [a b] (p: τ (sum a b) → Prop) (s: τ (sum a b)) :
65+
(Π x, π (s = inl x) → π (p s)) → (Π y, π (s = inr y) → π (p s)) → π (p s) ≔
66+
begin
67+
assume a b p s hl hr; refine ∨ₑ (case_Sum s) (λ h, ∃ₑ h hl) (λ h, ∃ₑ h hr)
68+
end;
69+
70+
symbol map_sum [a b c d] (f: τ a → τ c) (g: τ b → τ d) (s: τ (sum a b))
71+
: τ (sum c d) ≔ sum_case s (λ x, inl (f x)) (λ y, inr (g y));
72+
73+
opaque symbol map_sum_id [a b] (s: τ (sum a b)) :
74+
π (map_sum (λ u, u) (λ v, v) s = s) ≔
75+
begin assume a b s; refine η_sum s end;
76+
77+
opaque symbol map_sum_comp [a b c d e f]
78+
(g: τ c → τ e) (g': τ d → τ f) (h: τ a → τ c) (h': τ b → τ d) (s: τ (sum a b)) :
79+
π (map_sum g g' (map_sum h h' s) = map_sum (λ u, g (h u)) (λ v, g' (h' v)) s) ≔
80+
begin
81+
assume a b c d e f g g' h h';
82+
induction { reflexivity } { reflexivity }
83+
end;
84+
85+
symbol swap_sum [a b] (s: τ (sum a b)) : τ (sum b a) ≔
86+
sum_case s (λ x, inr x) (λ y, inl y);
87+
88+
opaque symbol swap_sum_invol [a b] (s: τ (sum a b)) :
89+
π (swap_sum (swap_sum s) = s) ≔
90+
begin
91+
assume a b; induction { reflexivity } { reflexivity }
92+
end;
93+
94+
// currying
95+
96+
symbol sum_curry₁ [a b c] (h: τ (sum a b) → τ c) (x: τ a) : τ c ≔ h (inl x);
97+
symbol sum_curry₂ [a b c] (h: τ (sum a b) → τ c) (y: τ b) : τ c ≔ h (inr y);
98+
99+
symbol sum_uncurry [a b c] (f: τ a → τ c) (g: τ b → τ c) (s: τ (sum a b)) : τ c ≔
100+
sum_case s f g;
101+
102+
opaque symbol sum_uncurry_curry [a b c] (h: τ (sum a b) → τ c) (s: τ (sum a b)) :
103+
π (sum_uncurry (sum_curry₁ h) (sum_curry₂ h) s = h s) ≔
104+
begin
105+
assume a b c h; induction { reflexivity } { reflexivity }
106+
end;
107+
108+
opaque symbol sum_curry_uncurry₁ [a b c] (f: τ a → τ c) (g: τ b → τ c) (x: τ a) :
109+
π (sum_curry₁ (sum_uncurry f g) x = f x) ≔
110+
begin reflexivity end;
111+
112+
opaque symbol sum_curry_uncurry₂ [a b c] (f: τ a → τ c) (g: τ b → τ c) (y: τ b) :
113+
π (sum_curry₂ (sum_uncurry f g) y = g y) ≔
114+
begin reflexivity end;
115+
116+
// Relation between the product and the coproduct
117+
118+
require open Stdlib.Prod;
119+
120+
symbol dist_× [a b c] (x: τ (a × sum b c)) : τ (sum (a × b) (a × c)) ≔
121+
sum_case (x ₂) (λ y, inl ((x ₁) ‚ y)) (λ z, inr ((x ₁) ‚ z));
122+
123+
symbol undist_× [a b c] (s: τ (sum (a × b) (a × c))) : τ (a × sum b c) ≔
124+
sum_case s (λ u, (u ₁) ‚ inl (u ₂)) (λ v, (v ₁) ‚ inr (v ₂));
125+
126+
opaque symbol undist_dist_‚ [a b c] (u: τ a) (s: τ (sum b c)) :
127+
π (undist_× (dist_× (u ‚ s)) = u ‚ s) ≔
128+
begin
129+
assume a b c u; induction { reflexivity } { reflexivity }
130+
end;
131+
132+
opaque symbol undist_dist_× [a b c] (x: τ (a × sum b c)) :
133+
π (undist_× (dist_× x) = x) ≔
134+
begin
135+
assume a b c x; rewrite prodExt x; refine undist_dist_‚ (x ₁) (x ₂)
136+
end;
137+
138+
opaque symbol dist_undist_× [a b c] (s: τ (sum (a × b) (a × c))) :
139+
π (dist_× (undist_× s) = s) ≔
140+
begin
141+
assume a b c; induction
142+
{ assume u; symmetry; refine feq inl (prodExt u) }
143+
{ assume v; symmetry; refine feq inr (prodExt v) }
144+
end;

‎DepProd.lp‎

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
// Dependent product: a dependent pair of an element and an element in Set
2+
3+
require open Stdlib.Eq;
4+
5+
[a: Set] (p: τ a → Set) inductive DProd : TYPE ≔
6+
dpair (x: τ a) : τ (p x) → DProd p;
7+
8+
constant symbol dprod [a: Set] : (τ a → Set) → Set;
9+
10+
rule τ (@dprod $a $p) ↪ @DProd $a $p;
11+
12+
symbol proj₁ [a] [p] (e: @DProd a p) : τ a;
13+
14+
rule proj₁ (dpair $x _) ↪ $x;
15+
16+
symbol proj₂ [a] [p] (e: @DProd a p) : τ (p (proj₁ e));
17+
18+
rule proj₂ (dpair _ $u) ↪ $u;
19+
20+
opaque symbol η_dprod [a] [p] (e: @DProd a p) :
21+
π (dpair (proj₁ e) (proj₂ e) = e) ≔
22+
begin assume a p; induction; assume x u; reflexivity end;
23+
24+
opaque symbol eq_proj₁ [a] [p] (x y: @DProd a p) :
25+
π (x = y) → π (proj₁ x = proj₁ y) ≔
26+
begin assume a p x y h; refine feq (λ e, proj₁ e) h end;
27+
28+
opaque symbol eq_dpair_refl [a] [p] (x: τ a) (u v: τ (p x)) :
29+
π (u = v) → π (@dpair a p x u = dpair x v) ≔
30+
begin
31+
assume a p x u v h; refine feq (λ w, @dpair a p x w) h
32+
end;
33+
34+
symbol transport [a] (p: τ a → Set) [x y: τ a] : π (x = y) → τ (p x) → τ (p y);
35+
rule transport _ (eq_refl _) $u ↪ $u;
36+
37+
symbol eq_dpair [a] [p] (x y: τ a) (u: τ (p x)) (v: τ (p y)) (h: π (x = y)) :
38+
π (transport p h u = v) → π (@dpair a p x u = dpair y v);

‎Epsilon.lp‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,3 +2,8 @@ require open Stdlib.FOL;
22

33
symbol ε [a:Set] : (τ a → Prop) → τ a;
44
symbol εᵢ [a:Set] (p:τ a → Prop) : π (∃ p) → π (p (ε p));
5+
6+
opaque symbol εₑ [a:Set] (p:τ a → Prop) : π (p (ε p)) → π (`∃ x, p x) ≔
7+
begin
8+
assume a p h; refine ∃ᵢ (ε p) h
9+
end;

‎ExtraRules.lp‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -39,6 +39,7 @@ rule P.add $x P.H ↪ P.succ $x
3939
with P.add P.H $y ↪ P.succ $y;
4040
rule P.add_carry $x P.H ↪ P.add $x (P.O P.H)
4141
with P.add_carry P.H $y ↪ P.add (P.O P.H) $y;
42+
rule P.mul $x P.H ↪ $x;
4243

4344
// Z
4445

0 commit comments

Comments
 (0)