Add lemmas and definitions from Alethe development

Bool.lp: imp, xorb, if-then-else lemmas
Epsilon.lp: εₑ
HOL.lp: transport
List.lp: foldl/foldr, mergesort and its correctness
Nat.lp: parity, div2, bitwise ops, strong induction
Pos.lp: multiplication lemmas
Prod.lp: sum type, dependent pairs, product lemmas
Z.lp: multiplication, power, comparison lemmas

Author: NotBad4U

Bool.lp

@@ -104,6 +104,20 @@ begin
   { simplify; assume h0 h1; refine h1 }
 end;
 
+opaque symbol notK b : π (not (not b) = b) ≔
+begin
+  induction
+  { reflexivity }
+  { reflexivity }
+end;
+
+opaque symbol negb_false_eq_true b : π (not b = false ⇔ b = true) ≔
+begin
+induction
+{simplify; apply ∧ᵢ { assume h; reflexivity } { assume h; reflexivity }}
+{simplify; apply ∧ᵢ { assume h; apply ⊥ₑ (true≠false h) } { assume h; apply ⊥ₑ (false≠true h) }}
+end;
+
 // or
 
 symbol or : 𝔹 → 𝔹 → 𝔹;
@@ -129,6 +143,65 @@ begin
     {reflexivity}
 end;
 
+// imp
+
+symbol imp : 𝔹 → 𝔹 → 𝔹;
+
+notation imp infix left 20;
+
+rule true imp true ↪ true
+with true imp false ↪ false
+with false imp true ↪ true
+with false imp false ↪ true;
+
+opaque symbol ⇒_istrue [p q : 𝔹] : π(p imp q) → π(p ⇒ q) ≔
+begin
+  induction
+  { induction
+    {
+      simplify;
+      assume h1; refine (λ x, x)
+    }
+    {
+      simplify; assume h1 h2; refine h1
+    }
+  }
+  {
+    induction
+    {
+      simplify;
+      assume h1 h2; apply h1
+    }
+    {
+      simplify;
+      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 +299,110 @@ begin
   { assume q i; apply ⊥ₑ i; }
 end;
 
+// xorb
+
+symbol xorb : 𝔹 → 𝔹 → 𝔹;
+
+notation xorb infix left 22;
+
+rule false xorb false ↪ false
+with false xorb true ↪ true
+with true xorb false ↪ true
+with true xorb true ↪ false;
+
+opaque symbol xorbᵢ₁ [p q : 𝔹] : π p → π (not q) → π (p xorb q) ≔
+begin
+  induction
+  { induction
+    { simplify; assume h i; apply i }
+    { simplify; assume h i; apply ⊤ᵢ }
+  }
+  { induction
+    { simplify; assume h i; apply ⊥ₑ h }
+    { simplify; assume h i; apply ⊥ₑ h }
+  }
+end;
+
+opaque symbol xorbᵢ₂ [p q : 𝔹] : π (not p) → π q → π (p xorb q) ≔
+begin
+  induction
+  { induction
+    { simplify; assume h i; apply ⊥ₑ h }
+    { simplify; assume h i; apply ⊥ₑ h }
+  }
+  { induction
+    { simplify; assume h i; apply ⊤ᵢ }
+    { simplify; assume 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
+  { induction
+    { simplify; assume r h h1 h2; apply ⊥ₑ h }
+    { simplify; assume r h h1 h2; apply h1 ⊤ᵢ ⊤ᵢ }
+  }
+  { induction
+    { simplify; assume r h h1 h2; apply h2 ⊤ᵢ ⊤ᵢ }
+    { simplify; assume r h h1 h2; apply ⊥ₑ 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
+  assume a x y; reflexivity
+end;
+
+opaque symbol if_false [a] (x y : τ a) : π (if false x y = y) ≔
+begin
+  assume a x y; 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;
+

Epsilon.lp

@@ -1,4 +1,12 @@
-require open Stdlib.FOL;
+require open Stdlib.FOL Stdlib.FunExt Stdlib.Impred;
 
 symbol ε [a:Set] : (τ a → Prop) → τ a;
 symbol εᵢ [a:Set] (p:τ a → Prop) : π (∃ p) → π (p (ε p));
+
+opaque symbol εₑ [a:Set] (p:τ a → Prop) : π (p (ε p)) → π (∃ p) ≔
+begin
+  assume a p h;
+  have e : π ((λ x, p x) = p) { refine funExt (λ x, p x) p (λ x, eq_refl (p x)) };
+  rewrite left e;
+  refine ∃ᵢ (ε p) h
+end;

HOL.lp

@@ -1,4 +1,4 @@
-require open Stdlib.Set;
+require open Stdlib.Set Stdlib.Eq;
 
 constant symbol ⤳ : Set → Set → Set; // \leadsto
 
@@ -18,3 +18,8 @@ rule τ ($a ⤳d λ x,$b.[x]) ↪ Π x:τ $a, τ $b.[x];
 symbol ∘ [a b c] : τ (b ⤳ c) → τ (a ⤳ b) → τ a → τ c ≔ λ g f x, g (f x);
 
 notation ∘ infix 20;
+
+symbol transport [a] (p: τ a → Set) [x y: τ a] : π (x = y) → τ (p x) → τ (p y);
+
+rule @transport _ _ $x $x _ $u ↪ $u
+with @transport _ (λ _, _) _ _ _ $u ↪ $u;