Add lemmas to check the validity of extra rules

Bool.lp

@@ -15,8 +15,8 @@ rule τ bool ↪ 𝔹;
 opaque symbol case_𝔹 b : π (b = true ∨ b = false) ≔
 begin
   induction
-  { apply ∨ᵢ₁; reflexivity; }
-  { apply ∨ᵢ₂; reflexivity; }
+  { apply ∨ᵢ₁; reflexivity }
+  { apply ∨ᵢ₂; reflexivity }
 end;
 
 opaque symbol ind_𝔹_eq p b:
@@ -115,12 +115,12 @@ opaque symbol not_inj [b c] : π (not b = not c) → π (b = c) ≔
 begin
   induction
   { induction
-    { assume h; reflexivity }
+    { reflexivity }
     { assume h; apply ⊥ₑ (false≠true h) }
   }
   { induction
     { assume h; apply ⊥ₑ (true≠false h) }
-    { assume h; reflexivity }
+    { reflexivity }
   }
 end;
 
@@ -133,21 +133,11 @@ notation or infix left 20;
 rule true  or _     ↪ true
 with false or $b    ↪ $b;
 
-opaque symbol or_true_lhs [p : 𝔹] :
-  π ((p or true) = true) ≔
-begin
-  induction
-    {reflexivity}
-    {reflexivity}
-end;
+opaque symbol or_true b: π(b or true = true) ≔
+begin induction {reflexivity} {reflexivity} end;
 
-opaque symbol or_false_lhs [p : 𝔹] :
-  π ((p or false) = p) ≔
-begin
-  induction
-    {reflexivity}
-    {reflexivity}
-end;
+opaque symbol or_false b: π(b or false = b) ≔
+begin induction {reflexivity} {reflexivity} end;
 
 // imp
 
@@ -195,15 +185,15 @@ end;
 opaque symbol ∨_istrue [p q : 𝔹] : π(p or q) → π(p ∨ q) ≔
 begin
   induction
-  { assume q h; apply ∨ᵢ₁; apply ⊤ᵢ; }
-  { assume q h; apply ∨ᵢ₂; apply h; }
+  { assume q h; apply ∨ᵢ₁; apply ⊤ᵢ }
+  { assume q h; apply ∨ᵢ₂; apply h }
 end;
 
 opaque symbol istrue_or [p q : 𝔹] : π(p ∨ q) → π(p or q) ≔
 begin
   induction
-  { assume q h; apply ⊤ᵢ; }
-  { assume q h; apply ∨ₑ h { assume i; apply ⊥ₑ i; } { assume i; apply i; } }
+  { assume q h; apply ⊤ᵢ }
+  { assume q h; apply ∨ₑ h { assume i; apply ⊥ₑ i } { assume i; apply i } }
 end;
 
 opaque symbol orᵢ₁ [p : 𝔹] q : π p → π (p or q) ≔
@@ -231,43 +221,47 @@ end;
 opaque symbol orC p q : π (p or q = q or p) ≔
 begin
     induction
-    { assume q; rewrite or_true_lhs [q]; reflexivity }
-    { assume q; rewrite or_false_lhs [q]; reflexivity }
+    { assume q; rewrite or_true; reflexivity }
+    { assume q; rewrite or_false; reflexivity }
 end;
 
 opaque symbol orA p q r : π ((p or q) or r = p or (q or r)) ≔
 begin
     induction
-    { reflexivity; }
-    { reflexivity; }
+    { reflexivity }
+    { reflexivity }
 end;
 
 // and
 
 symbol and : 𝔹 → 𝔹 → 𝔹;
 
-notation and infix left 7;
+notation and infix left 15;
 
 rule true  and $b    ↪ $b
-with $b    and true  ↪ $b
-with false and _     ↪ false
-with _     and false ↪ false;
+with false and _     ↪ false;
+
+opaque symbol and_true b: π(b and true = b) ≔
+begin induction {reflexivity} {reflexivity} end;
+
+opaque symbol and_false b: π(b and false = false) ≔
+begin induction {reflexivity} {reflexivity} end;
 
 opaque symbol ∧_istrue [p q : 𝔹] : π(p and q) → π(p ∧ q) ≔
 begin
   induction
   { induction
     { assume h; apply ∧ᵢ { apply ⊤ᵢ } { apply ⊤ᵢ } }
-    { assume h; apply ⊥ₑ h; }
+    { assume h; apply ⊥ₑ h }
   }
-  { assume q h; apply ⊥ₑ h; }
+  { assume q h; apply ⊥ₑ h }
 end;
 
 opaque symbol istrue_and [p q : 𝔹] : π(p ∧ q) → π(p and q) ≔
 begin
   induction
-  { assume q h; apply ∧ₑ₂ h; }
-  { assume q h; apply ∧ₑ₁ h; }
+  { assume q h; apply ∧ₑ₂ h }
+  { assume q h; apply ∧ₑ₁ h }
 end;
 
 opaque symbol andᵢ [p q : 𝔹] : π p → π q → π(p and q) ≔
@@ -278,15 +272,15 @@ end;
 opaque symbol andₑ₁ [p q : 𝔹] : π (p and q) → π p ≔
 begin
   induction
-  { assume q i; apply ⊤ᵢ; }
-  { assume q i; apply i; }
+  { assume q i; apply ⊤ᵢ }
+  { assume q i; apply i }
 end;
 
 opaque symbol andₑ₂ [p q : 𝔹] : π (p and q) → π q ≔
 begin
   induction
-  { assume q i; apply i; }
-  { assume q i; apply ⊥ₑ i; }
+  { assume q i; apply i }
+  { assume q i; apply ⊥ₑ i }
 end;
 
 // xorb

Comp.lp

@@ -74,7 +74,7 @@ with opp Gt ↪ Lt;
 
 opaque symbol opp_idem c : π (opp (opp c) = c) ≔
 begin
-  induction { reflexivity; } { reflexivity; } { reflexivity; }
+  induction { reflexivity } { reflexivity } { reflexivity }
 end;
 
 // Conditional

DepProd.lp

@@ -19,7 +19,7 @@ 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;
+begin assume a p; induction; reflexivity end;
 
 opaque symbol eq_proj₁ [a] [p] (x y: @DProd a p) :
   π (x = y) → π (proj₁ x = proj₁ y) ≔

ExtraRules.lp

@@ -1,46 +1,99 @@
 // This module turns proved equalities to rewrite rules
 
+// Bool
+
 require open Stdlib.Bool;
-require Stdlib.Nat as N;
-require open Stdlib.List;
-require Stdlib.Pos as P;
-require Stdlib.Z as Z;
 
-// Bool
+opaque symbol or_true b:π(b or true = true) ≔ or_true b;
+rule _ or true  ↪ true;
 
-rule _ or true  ↪ true
-with $b or false ↪ $b;
+opaque symbol or_false b:π(b or false = b) ≔ or_false b;
+rule $b or false ↪ $b;
+
+opaque symbol and_true b:π(b and true = b) ≔ and_true b;
+rule $b and true ↪ $b;
+
+opaque symbol and_false b:π(b and false = false) ≔ and_false b;
+rule _ and false ↪ false;
 
 // Nat
 
-rule $x N.+ N._0 ↪ $x;
-rule $x N.+ $y N.+1 ↪ ($x N.+ $y) N.+1;
-rule ($x N.+ $y) N.+ $z ↪ $x N.+ ($y N.+ $z);
-rule $x N.- N._0 ↪ $x;
-rule _ N.* N._0 ↪ N._0;
-rule N.max $x N._0 ↪ $x;
-rule N.max $x $x ↪ $x;
-rule N.min _ N._0 ↪ N._0;
-rule N.min $x $x ↪ $x;
+require open Stdlib.Nat;
+
+opaque symbol addn0 x: π(x + _0 = x) ≔ addn0 x;
+rule $x + _0 ↪ $x;
+
+opaque symbol addnS x y: π(x + y +1 = (x + y) +1) ≔ addnS x y;
+rule $x + $y +1 ↪ ($x + $y) +1;
+
+opaque symbol addnA x y z: π((x + y) + z = x + (y + z)) ≔ addnA x y z;
+rule ($x + $y) + $z ↪ $x + ($y + $z);
+
+opaque symbol subn0 x: π(x - _0 = x) ≔ subn0 x;
+rule $x - _0 ↪ $x;
+
+opaque symbol muln0 x: π(x * _0 = _0) ≔ muln0 x;
+rule _ * _0 ↪ _0;
+
+opaque symbol maxn0 x: π(max x _0 = x) ≔ maxn0 x;
+rule max $x _0 ↪ $x;
+
+opaque symbol maxnn x: π(max x x = x) ≔ maxnn x;
+rule max $x $x ↪ $x;
+
+opaque symbol minn0 x: π(min x _0 = 0) ≔ minn0 x;
+rule min _ _0 ↪ _0;
+
+opaque symbol minnn x: π(min x x = x) ≔ minnn x;
+rule min $x $x ↪ $x;
 
 // List
 
+require open Stdlib.List;
+
+opaque symbol cats0 a (m:𝕃 a): π(m ++ □ = m) ≔ cats0 m;
 rule $m ++ □ ↪ $m;
-rule size ($l ++ $m) ↪ size $l N.+ size $m;
+
+opaque symbol size_cat a (l m:𝕃 a): π(size(l ++ m) = size l + size m) ≔ size_cat l m;
+rule size ($l ++ $m) ↪ size $l + size $m;
+
+opaque symbol catA a (l m n:𝕃 a): π((l ++ m) ++ n = l ++ (m ++ n)) ≔ catA l m n;
 rule ($l ++ $m) ++ $n ↪ $l ++ ($m ++ $n);
+
+opaque symbol lastl a x e (l:𝕃 a): π(last x (e ⸬ l) = last e l) ≔ lastl l x e;
 rule last _ ($e ⸬ $l) ↪ last $e $l;
+
+opaque symbol nthx□ a (x:τ a) n: π(nth x □ n = x) ≔ nthx□ n x;
 rule nth $x □ _ ↪ $x;
+
+opaque symbol dropx□ a n: π(drop n □ = □ [a]) ≔ dropx□ n;
 rule drop _ □ ↪ □;
+
+opaque symbol taken□ a n: π(take n □ = □ [a]) ≔ taken□ n;
 rule take _ □ ↪ □;
 
 // Pos
 
-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;
+require open Stdlib.Pos;
+
+opaque symbol addnH x: π(add x H = succ x) ≔ addnH x;
+rule add $x H ↪ succ $x;
+
+opaque symbol addHn y: π(add H y = succ y) ≔ addHn y;
+rule add H $y ↪ succ $y;
+
+opaque symbol ad_carrynH x: π(add_carry x H = add x (O H)) ≔ add_carrynH x;
+rule add_carry $x H ↪ add $x (O H);
+
+opaque symbol add_carryHn y: π(add_carry H y = add (O H) y) ≔ add_carryHn y;
+rule add_carry H $y ↪ add (O H) $y;
+
+opaque symbol mul_H_right x: π(mul x H = x) ≔ mul_H_right x;
+rule mul $x H ↪ $x;
 
 // Z
 
-rule $x Z.+ Z.Z0 ↪ $x;
+require open Stdlib.Z;
+
+opaque symbol +Z0 x: π(x + Z0 = x) ≔ +Z0 x;
+rule $x + Z0 ↪ $x;