cleaning (#44)

Author: fblanqui

List.lp

@@ -873,11 +873,6 @@ begin
   }
 end;
 
-opaque symbol size_take [a] n (l:𝕃 a) :
-  π (size (take n l) = if (n < size l) n (size l)) ≔
-begin
-abort;
-
 opaque symbol size_take_min [a] n (l:𝕃 a) :
   π (size (take n l) = min n (size l)) ≔
 begin
@@ -1037,15 +1032,6 @@ begin
   assume a l; simplify; rewrite take_size l; rewrite @drop_size a; reflexivity;
 end;
 
-opaque symbol rotK [a] n (l:𝕃 a) : π (rot n (rotr n l) = l) ≔
-begin
-abort;
-
-opaque symbol rot_inj [a] n (l1 l2:𝕃 a) :
-  π (rot n l1 = rot n l2) → π (l1 = l2) ≔
-begin
-abort;
-
 // membership
 
 symbol ∈ [a] : (τ a → τ a → 𝔹) → τ a → 𝕃 a → 𝔹;
@@ -1424,11 +1410,6 @@ begin
   rewrite left size_cat (filter p l1) (filter p l2); reflexivity;
 end;
 
-opaque symbol eq_find [a] beq p (l1 l2:𝕃 a) :
-  π (eql beq l1 l2) → π (eqn (find p l1) (find p l2)) ≔
-begin
-abort;
-
 // undup
 
 symbol undup [a] : (τ a → τ a → 𝔹) → 𝕃 a → 𝕃 a;
@@ -1466,16 +1447,6 @@ begin
   }
 end;
 
-opaque symbol filter_undup [a] beq p (l:𝕃 a) :
-  π (filter p (undup beq l) = undup beq (filter p l)) ≔
-begin
-abort;
-
-opaque symbol count_undup [a] beq p (l:𝕃 a) :
-  π (count p (undup beq l) ≤ count p l) ≔
-begin
-abort;
-
 // map
 
 symbol map [a b] : (τ a → τ b) → 𝕃 a → 𝕃 b;

Nat.lp

@@ -833,10 +833,6 @@ begin
   }
 end;
 
-opaque symbol ltn_neqAle m n : π (istrue (m < n) ⇔ istrue (m ≤ n) ∧ (m ≠ n)) ≔
-begin
-abort;
-
 opaque symbol leq_add0 m n :
   π (istrue (_0 ≤ m)) → π (istrue (_0 ≤ n)) → π (istrue (_0 ≤ m + n)) ≔
 begin
@@ -1195,16 +1191,6 @@ begin
   assume m n; rewrite maxnC m n; apply leq_maxl n m;
 end;
 
-opaque symbol gtn_max m n1 n2 :
-  π (istrue (m > max n1 n2) ⇔ istrue (m > n1) ∧ istrue (m > n2)) ≔
-begin
-abort;
-
-opaque symbol geq_max m n1 n2 :
-  π (istrue (m ≥ max n1 n2) ⇔ istrue (m ≥ n1) ∧ istrue (m ≥ n2)) ≔
-begin
-abort;
-
 opaque symbol ltn_predK m n : π (istrue (m < n)) → π (n ∸1 +1 = n) ≔
 begin
   assume m; induction
@@ -1465,10 +1451,6 @@ begin
   }
 end;
 
-opaque symbol minnE m n : π (min m n = m - (m - n)) ≔
-begin
-abort;
-
 opaque symbol minnn x : π (min x x = x) ≔
 begin
   induction
@@ -1747,15 +1729,6 @@ begin
   reflexivity;
 end;
 
-opaque symbol expn_gt0 m n :
-  π ((istrue (_0 < m ^ n)) ⇔ istrue (_0 < m) ∨ (n = _0)) ≔
-begin
-abort;
-
-opaque symbol ltn_expl m n : π (istrue ((_0 +1) < m)) → π (istrue (n < m ^ n)) ≔
-begin
-abort;
-
 // factorial
 
 symbol ! : ℕ → ℕ; notation ! postfix 40;
@@ -1811,8 +1784,6 @@ symbol _10 ≔ _9 +1;
 builtin "nat_zero" ≔ _0;
 builtin "nat_succ" ≔ +1;
 
-compute _2 + _2;
-
 // enable parsing of natural numbers in decimal notation
 
 builtin "0"  ≔ _0;
@@ -1829,5 +1800,3 @@ builtin "10" ≔ _10;
 
 builtin "+" ≔ +;
 builtin "*" ≔ *;
-
-type 42;

Pos.lp

@@ -580,5 +580,3 @@ symbol _10 ≔ O (I (O H));
 builtin "pos_one" ≔ H;
 builtin "pos_double" ≔ O;
 builtin "pos_succ_double" ≔ I;
-
-compute add _2 _2;