Add lemmas and definitions from Alethe development

Bool.lp

@@ -104,6 +104,26 @@ begin
   { simplify; assume h0 h1; refine h1 }
 end;
 
+opaque symbol notK b : π (not (not b) = b) ≔
+begin
+  induction
+  { reflexivity }
+  { reflexivity }
+end;
+
+opaque symbol not_inj [b c] : π (not b = not c) → π (b = c) ≔
+begin
+  induction
+  { induction
+    { assume h; reflexivity }
+    { assume h; apply ⊥ₑ (false≠true h) }
+  }
+  { induction
+    { assume h; apply ⊥ₑ (true≠false h) }
+    { assume h; reflexivity }
+  }
+end;
+
 // or
 
 symbol or : 𝔹 → 𝔹 → 𝔹;
@@ -129,6 +149,49 @@ begin
     {reflexivity}
 end;
 
+// imp
+
+symbol imp (b c : 𝔹) : 𝔹 ≔ not b or c;
+
+notation imp infix left 20;
+
+opaque symbol ⇒_istrue [p q : 𝔹] : π(p imp q) → π(p ⇒ q) ≔
+begin
+  induction
+  { induction
+    { assume h1; refine (λ x, x) }
+    { assume h1 h2; refine h1 }
+  }
+  {
+    induction
+    { assume h1 h2; apply h1 }
+    { assume h1; refine (λ x, x) }
+   }
+end;
+
+opaque symbol istrue_imp [p q : 𝔹] : π(p ⇒ q) → π(p imp q) ≔
+begin
+  induction
+  { induction
+    { assume h; apply ⊤ᵢ }
+    { assume h; apply h ⊤ᵢ }
+  }
+  { induction
+    { assume h; apply ⊤ᵢ }
+    { assume h; apply ⊤ᵢ }
+  }
+end;
+
+opaque symbol impᵢ [p q : 𝔹] : (π p → π q) → π (p imp q) ≔
+begin
+  assume p q h; apply @istrue_imp p q h;
+end;
+
+opaque symbol impₑ [p q : 𝔹] : π (p imp q) → π p → π q ≔
+begin
+  assume p q h; refine @⇒_istrue p q h;
+end;
+
 opaque symbol ∨_istrue [p q : 𝔹] : π(p or q) → π(p ∨ q) ≔
 begin
   induction
@@ -226,9 +289,86 @@ begin
   { assume q i; apply ⊥ₑ i; }
 end;
 
+// xorb
+
+symbol xorb : 𝔹 → 𝔹 → 𝔹;
+
+notation xorb infix left 22;
+
+rule false xorb $b ↪ $b
+with true xorb $b ↪ not $b;
+
+opaque symbol xorbᵢ₁ [p q : 𝔹] : π p → π (not q) → π (p xorb q) ≔
+begin
+  induction
+  { assume q h i; apply i }
+  { assume q h i; apply ⊥ₑ h }
+end;
+
+opaque symbol xorbᵢ₂ [p q : 𝔹] : π (not p) → π q → π (p xorb q) ≔
+begin
+  induction
+  { assume q h i; apply ⊥ₑ h }
+  { assume q h i; apply i }
+end;
+
+opaque symbol xorbₑ [p q : 𝔹] (r : 𝔹) :
+  π (p xorb q) → (π p → π (not q) → π r) → (π (not p) → π q → π r) → π r ≔
+begin
+  induction
+  { assume q r h h1 h2; apply h1 ⊤ᵢ h }
+  { assume q r h h1 h2; apply h2 ⊤ᵢ h }
+end;
+
 // if-then-else
 
 symbol if : 𝔹 → Π [a], τ a → τ a → τ a;
 
 rule if true  $x _ ↪ $x
 with if false _ $y ↪ $y;
+
+opaque symbol if_true [a] (x y : τ a) : π (if true x y = x) ≔
+begin reflexivity end;
+
+opaque symbol if_false [a] (x y : τ a) : π (if false x y = y) ≔
+begin reflexivity end;
+
+opaque symbol if_same b [a] (x : τ a) : π (if b x x = x) ≔
+begin
+  assume b a x;
+  refine ∨ₑ (case_𝔹 b) _ _
+    { assume h; rewrite h; reflexivity }
+    { assume h; rewrite h; reflexivity }
+end;
+
+opaque symbol if_id b : π (if b true false = b) ≔
+begin
+  induction
+  { reflexivity }
+  { reflexivity }
+end;
+
+opaque symbol if_not b [a] (x y : τ a) : π (if (not b) x y = if b y x) ≔
+begin
+  assume b a x y;
+  refine ∨ₑ (case_𝔹 b) _ _
+    { assume h; rewrite h; reflexivity }
+    { assume h; rewrite h; reflexivity }
+end;
+
+opaque symbol if_istrue [b : 𝔹] [a] (x y : τ a) : π b → π (if b x y = x) ≔
+begin
+  assume b a x y h;
+  refine ∨ₑ (case_𝔹 b) _ _
+    { assume h1; rewrite h1; reflexivity }
+    { assume h1; apply ⊥ₑ (false=¬istrue h1 h) }
+end;
+
+opaque symbol if_isfalse [b : 𝔹] [a] (x y : τ a) : π (not b) → π (if b x y = y) ≔
+begin
+  assume b a x y h;
+  refine ∨ₑ (case_𝔹 b) _ _
+    { assume h1; apply ⊥ₑ (istrue_not h (true=istrue h1)) }
+    { assume h1; rewrite h1; reflexivity }
+end;
+

CHANGES.md

@@ -11,6 +11,16 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 - Univ: universe levels for Set and Prop
 - Quotient: quotient types
 - NaryFun: n-ary functions and relations
+- 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
 
 ### Changed
 

Coprod.lp

@@ -0,0 +1,144 @@
+// Co-Cartesian product (disjoint sum)
+
+require open Stdlib.FOL Stdlib.Eq;
+
+(a: Set) (b: Set) inductive Sum: TYPE ≔
+| inl: τ a → Sum a b
+| inr: τ b → Sum a b;
+
+constant symbol sum : Set → Set → Set;
+
+rule τ (sum $a $b) ↪ Sum $a $b;
+
+// Universal property: a map out of a sum is given by case analysis
+
+symbol sum_case [a b c] : τ (sum a b) → (τ a → τ c) → (τ b → τ c) → τ c;
+
+rule sum_case (inl $x) $f _ ↪ $f $x
+with sum_case (inr $y) _ $g ↪ $g $y;
+
+opaque symbol sum_case_uniq [a b c] (h: τ (sum a b) → τ c) (s: τ (sum a b)) :
+  π (sum_case s (λ x, h (inl x)) (λ y, h (inr y)) = h s) ≔
+begin
+  assume a b c h; induction { reflexivity } { reflexivity }
+end;
+
+opaque symbol η_sum [a b] (s: τ (sum a b)) :
+  π (sum_case s (λ x, inl x) (λ y, inr y) = s) ≔
+begin
+  assume a b; induction { reflexivity } { reflexivity }
+end;
+
+// non confusion of constructors
+
+symbol is_inl [a b] : τ (sum a b) → Prop;
+
+rule is_inl (inl _) ↪ ⊤
+with is_inl (inr _) ↪ ⊥;
+
+opaque symbol inr≠inl [a b] (x: τ a) (y: τ b) : π (@inr a b y ≠ inl x) ≔
+begin assume a b x y h; refine ind_eq h (λ s, is_inl s) ⊤ᵢ end;
+
+opaque symbol inl≠inr [a b] (x: τ a) (y: τ b) : π (@inl a b x ≠ inr y) ≔
+begin assume a b x y h; apply inr≠inl x y; symmetry; apply h end;
+
+symbol outl [a b] (s: τ (sum a b)) : τ a ≔ sum_case s (λ x, x) (λ _, el a);
+symbol outr [a b] (s: τ (sum a b)) : τ b ≔ sum_case s (λ _, el b) (λ y, y);
+
+opaque symbol inl_inj [a b] (x x': τ a) : π (@inl a b x = inl x') → π (x = x') ≔
+begin assume a b x x' h; refine feq (λ s, @outl a b s) h end;
+
+opaque symbol inr_inj [a b] (y y': τ b) : π (@inr a b y = inr y') → π (y = y') ≔
+begin assume a b y y' h; refine feq (λ s, @outr a b s) h end;
+
+// induction principle with equalities
+
+opaque symbol case_Sum [a b] (s: τ (sum a b)) :
+  π ((`∃ x, s = inl x) ∨ (`∃ y, s = inr y)) ≔
+begin
+  assume a b; induction
+  { assume x; apply ∨ᵢ₁; apply ∃ᵢ x; reflexivity }
+  { assume y; apply ∨ᵢ₂; apply ∃ᵢ y; reflexivity }
+end;
+
+opaque symbol ind_Sum_eq [a b] (p: τ (sum a b) → Prop) (s: τ (sum a b)) :
+  (Π x, π (s = inl x) → π (p s)) → (Π y, π (s = inr y) → π (p s)) → π (p s) ≔
+begin
+  assume a b p s hl hr; refine ∨ₑ (case_Sum s) (λ h, ∃ₑ h hl) (λ h, ∃ₑ h hr)
+end;
+
+symbol map_sum [a b c d] (f: τ a → τ c) (g: τ b → τ d) (s: τ (sum a b))
+  : τ (sum c d) ≔ sum_case s (λ x, inl (f x)) (λ y, inr (g y));
+
+opaque symbol map_sum_id [a b] (s: τ (sum a b)) :
+  π (map_sum (λ u, u) (λ v, v) s = s) ≔
+begin assume a b s; refine η_sum s end;
+
+opaque symbol map_sum_comp [a b c d e f]
+  (g: τ c → τ e) (g': τ d → τ f) (h: τ a → τ c) (h': τ b → τ d) (s: τ (sum a b)) :
+  π (map_sum g g' (map_sum h h' s) = map_sum (λ u, g (h u)) (λ v, g' (h' v)) s) ≔
+begin
+  assume a b c d e f g g' h h';
+  induction { reflexivity } { reflexivity }
+end;
+
+symbol swap_sum [a b] (s: τ (sum a b)) : τ (sum b a) ≔
+  sum_case s (λ x, inr x) (λ y, inl y);
+
+opaque symbol swap_sum_invol [a b] (s: τ (sum a b)) :
+  π (swap_sum (swap_sum s) = s) ≔
+begin
+  assume a b; induction { reflexivity } { reflexivity }
+end;
+
+// currying
+
+symbol sum_curry₁ [a b c] (h: τ (sum a b) → τ c) (x: τ a) : τ c ≔ h (inl x);
+symbol sum_curry₂ [a b c] (h: τ (sum a b) → τ c) (y: τ b) : τ c ≔ h (inr y);
+
+symbol sum_uncurry [a b c] (f: τ a → τ c) (g: τ b → τ c) (s: τ (sum a b)) : τ c ≔
+  sum_case s f g;
+
+opaque symbol sum_uncurry_curry [a b c] (h: τ (sum a b) → τ c) (s: τ (sum a b)) :
+  π (sum_uncurry (sum_curry₁ h) (sum_curry₂ h) s = h s) ≔
+begin
+  assume a b c h; induction { reflexivity } { reflexivity }
+end;
+
+opaque symbol sum_curry_uncurry₁ [a b c] (f: τ a → τ c) (g: τ b → τ c) (x: τ a) :
+  π (sum_curry₁ (sum_uncurry f g) x = f x) ≔
+begin reflexivity end;
+
+opaque symbol sum_curry_uncurry₂ [a b c] (f: τ a → τ c) (g: τ b → τ c) (y: τ b) :
+  π (sum_curry₂ (sum_uncurry f g) y = g y) ≔
+begin reflexivity end;
+
+// Relation between the product and the coproduct
+
+require open Stdlib.Prod;
+
+symbol dist_× [a b c] (x: τ (a × sum b c)) : τ (sum (a × b) (a × c)) ≔
+  sum_case (x ₂) (λ y, inl ((x ₁) ‚ y)) (λ z, inr ((x ₁) ‚ z));
+
+symbol undist_× [a b c] (s: τ (sum (a × b) (a × c))) : τ (a × sum b c) ≔
+  sum_case s (λ u, (u ₁) ‚ inl (u ₂)) (λ v, (v ₁) ‚ inr (v ₂));
+
+opaque symbol undist_dist_‚ [a b c] (u: τ a) (s: τ (sum b c)) :
+  π (undist_× (dist_× (u ‚ s)) = u ‚ s) ≔
+begin
+  assume a b c u; induction { reflexivity } { reflexivity }
+end;
+
+opaque symbol undist_dist_× [a b c] (x: τ (a × sum b c)) :
+  π (undist_× (dist_× x) = x) ≔
+begin
+  assume a b c x; rewrite prodExt x; refine undist_dist_‚ (x ₁) (x ₂)
+end;
+
+opaque symbol dist_undist_× [a b c] (s: τ (sum (a × b) (a × c))) :
+  π (dist_× (undist_× s) = s) ≔
+begin
+  assume a b c; induction
+  { assume u; symmetry; refine feq inl (prodExt u) }
+  { assume v; symmetry; refine feq inr (prodExt v) }
+end;

DepProd.lp

@@ -0,0 +1,38 @@
+// Dependent product: a dependent pair of an element and an element in Set
+
+require open Stdlib.Eq;
+
+[a: Set] (p: τ a → Set) inductive DProd : TYPE ≔
+  dpair (x: τ a) : τ (p x) → DProd p;
+
+constant symbol dprod [a: Set] : (τ a → Set) → Set;
+
+rule τ (@dprod $a $p) ↪ @DProd $a $p;
+
+symbol proj₁ [a] [p] (e: @DProd a p) : τ a;
+
+rule proj₁ (dpair $x _) ↪ $x;
+
+symbol proj₂ [a] [p] (e: @DProd a p) : τ (p (proj₁ e));
+
+rule proj₂ (dpair _ $u) ↪ $u;
+
+opaque symbol η_dprod [a] [p] (e: @DProd a p) :
+  π (dpair (proj₁ e) (proj₂ e) = e) ≔
+begin assume a p; induction; assume x u; reflexivity end;
+
+opaque symbol eq_proj₁ [a] [p] (x y: @DProd a p) :
+  π (x = y) → π (proj₁ x = proj₁ y) ≔
+begin assume a p x y h; refine feq (λ e, proj₁ e) h end;
+
+opaque symbol eq_dpair_refl [a] [p] (x: τ a) (u v: τ (p x)) :
+  π (u = v) → π (@dpair a p x u = dpair x v) ≔
+begin
+  assume a p x u v h; refine feq (λ w, @dpair a p x w) h
+end;
+
+symbol transport [a] (p: τ a → Set) [x y: τ a] : π (x = y) → τ (p x) → τ (p y);
+rule transport _ (eq_refl _) $u ↪ $u;
+
+symbol eq_dpair [a] [p] (x y: τ a) (u: τ (p x)) (v: τ (p y)) (h: π (x = y)) :
+  π (transport p h u = v) → π (@dpair a p x u = dpair y v);

Epsilon.lp

@@ -2,3 +2,8 @@ require open Stdlib.FOL;
 
 symbol ε [a:Set] : (τ a → Prop) → τ a;
 symbol εᵢ [a:Set] (p:τ a → Prop) : π (∃ p) → π (p (ε p));
+
+opaque symbol εₑ [a:Set] (p:τ a → Prop) : π (p (ε p)) → π (`∃ x, p x) ≔
+begin
+  assume a p h; refine ∃ᵢ (ε p) h
+end;

ExtraRules.lp

@@ -39,6 +39,7 @@ rule P.add $x P.H ↪ P.succ $x
 with P.add P.H $y ↪ P.succ $y;
 rule P.add_carry $x P.H ↪ P.add $x (P.O P.H)
 with P.add_carry P.H $y ↪ P.add (P.O P.H) $y;
+rule P.mul $x P.H ↪ $x;
 
 // Z