Structured proofs (#2)

Update proof scripts according to Deducteam/lambdapi#717.

Author: fblanqui

Bool.lp

@@ -43,7 +43,7 @@ with _     and false ↪ false;
 
 // Conditional
 
-symbol if : 𝔹 → Π {a}, τ a → τ a → τ a;
+symbol if : 𝔹 → Π [a], τ a → τ a → τ a;
 
 rule if true  $x _ ↪ $x
 with if false _ $y ↪ $y;

Eq.lp

@@ -2,37 +2,37 @@
 
 require open Stdlib.Set Stdlib.Prop;
 
-constant symbol = {a} : τ a → τ a → Prop;
+constant symbol = [a] : τ a → τ a → Prop;
 
 notation = infix 10;
 
-constant symbol eq_refl {a} (x:τ a) : π (x = x);
-constant symbol ind_eq {a} {x y:τ a} : π (x = y) → Π p, π (p y) → π (p x);
+constant symbol eq_refl [a] (x:τ a) : π (x = x);
+constant symbol ind_eq [a] [x y:τ a] : π (x = y) → Π p, π (p y) → π (p x);
 
 builtin "eq"    ≔ =;
 builtin "refl"  ≔ eq_refl;
 builtin "eqind" ≔ ind_eq;
 
 // inequality
 
-symbol ≠ {a} (x y : τ a) ≔ ¬ (x = y); // \neq
+symbol ≠ [a] (x y : τ a) ≔ ¬ (x = y); // \neq
 
 notation ≠ infix 1;
 
 // symmetry
 
-opaque symbol eq_sym {a} (x y:τ a) : π (x = y ⇒ y = x) ≔
+opaque symbol eq_sym [a] (x y:τ a) : π (x = y ⇒ y = x) ≔
 begin
   assume a x y xy;
   symmetry;
-  apply xy;
+  apply xy
 end;
 
 // monotony wrt function application
 
-opaque symbol feq {a b} (f:τ a → τ b) {x y:τ a} : π(x = y ⇒ f x = f y) ≔
+opaque symbol feq [a b] (f:τ a → τ b) [x y:τ a] : π(x = y ⇒ f x = f y) ≔
 begin
-assume a b f x y xy;
-apply ind_eq xy (λ z, f z = f y);
-reflexivity;
+  assume a b f x y xy;
+  apply ind_eq xy (λ z, f z = f y);
+  reflexivity
 end;

FOL.lp

@@ -4,19 +4,19 @@ require open Stdlib.Set Stdlib.Prop;
 
 // Universal quantification
 
-constant symbol ∀ {a} : (τ a → Prop) → Prop;
+constant symbol ∀ [a] : (τ a → Prop) → Prop;
 
 notation ∀ quantifier;
 
 rule π (∀ $f) ↪ Π x, π ($f x);
 
 // Existential quantification
 
-constant symbol ∃ {a} : (τ a → Prop) → Prop;
+constant symbol ∃ [a] : (τ a → Prop) → Prop;
 
 notation ∃ quantifier;
 
-constant symbol ∃ᵢ {a} p (x:τ a) : π (p x) → π (∃ p);
-symbol ∃ₑ {a} p : π (∃ p) → Π q, (Π x:τ a, π (p x) → π q) → π q;
+constant symbol ∃ᵢ [a] p (x:τ a) : π (p x) → π (∃ p);
+symbol ∃ₑ [a] p : π (∃ p) → Π q, (Π x:τ a, π (p x) → π q) → π q;
 
 rule ∃ₑ _ (∃ᵢ _ $x $px) _ $f ↪ $f $x $px;

List.lp

@@ -16,14 +16,14 @@ rule τ (list $a) ↪ 𝕃 $a;
 
 // Length of a list
 
-symbol length {a} : 𝕃 a → ℕ;
+symbol length [a] : 𝕃 a → ℕ;
 
 rule length □ ↪ 0
 with length (_ ⸬ $l) ↪ s (length $l);
 
 // Concatenation of two lists
 
-symbol ⋅ {a} : 𝕃 a → 𝕃 a → 𝕃 a;
+symbol ⋅ [a] : 𝕃 a → 𝕃 a → 𝕃 a;
 
 notation ⋅ infix right 15; // \cdot
 
@@ -33,82 +33,64 @@ assert a x l m ⊢ x ⸬ l ⋅ m ≡ x ⸬ (l ⋅ m);
 rule □ ⋅ $m ↪ $m
 with ($x ⸬ $l) ⋅ $m ↪ $x ⸬ ($l ⋅ $m);
 
-opaque symbol concat_nil {a} (l:𝕃 a) : π(l ⋅ □ = l) ≔
+opaque symbol concat_nil [a] (l:𝕃 a) : π(l ⋅ □ = l) ≔
 begin
-  assume a;
-  induction;
-  // case l = □
-  reflexivity;
-  // case l = x ⸬ l'
-  assume x l' h; simplify; rewrite h; reflexivity;
+  assume a; induction
+  { reflexivity }
+  { assume x l' h; simplify; rewrite h; reflexivity }
 end;
 
 rule $m ⋅ □ ↪ $m;
 
-opaque symbol length_concat {a} (l m : 𝕃 a) :
+opaque symbol length_concat [a] (l m : 𝕃 a) :
   π(length (l ⋅ m) = length l + length m) ≔
 begin
-  assume a;
-  induction;
-  // case l = □
-  reflexivity;
-  // case l = x⸬l'
-  assume x l' h m; simplify; rewrite h; reflexivity;
+  assume a; induction
+  { reflexivity }
+  { assume x l' h m; simplify; rewrite h; reflexivity }
 end;
 
 rule length ($l ⋅ $m) ↪ length $l + length $m;
 
-opaque symbol concat_assoc {a} (l m n : 𝕃 a) : π((l ⋅ m) ⋅ n = l ⋅ (m ⋅ n)) ≔
+opaque symbol concat_assoc [a] (l m n : 𝕃 a) : π((l ⋅ m) ⋅ n = l ⋅ (m ⋅ n)) ≔
 begin
-  assume a;
-  induction;
-  // case l = □
-  reflexivity;
-  // case l = x⸬l'
-  assume x l' h m n; simplify; rewrite h; reflexivity;
+  assume a; induction
+  { reflexivity }
+  { assume x l' h m n; simplify; rewrite h; reflexivity }
 end;
 
 rule ($l ⋅ $m) ⋅ $n ↪ $l ⋅ ($m ⋅ $n);
 
 // List reversal
 
-symbol rev {a} : 𝕃 a → 𝕃 a;
+symbol rev [a] : 𝕃 a → 𝕃 a;
 
 rule rev □ ↪ □
 with rev ($x ⸬ $l) ↪ rev $l ⋅ ($x ⸬ □);
 
-opaque symbol rev_concat {a} (l m : 𝕃 a) : π(rev (l ⋅ m) = rev m ⋅ rev l) ≔
+opaque symbol rev_concat [a] (l m : 𝕃 a) : π(rev (l ⋅ m) = rev m ⋅ rev l) ≔
 begin
-  assume a;
-  induction;
-  // case l = □
-  simplify; reflexivity;
-  // case l = ⸬
-  assume x l h m; simplify; rewrite h; reflexivity;
+  assume a; induction
+  { simplify; reflexivity }
+  { assume x l h m; simplify; rewrite h; reflexivity }
 end;
 
 rule rev ($l ⋅ $m) ↪ rev $m ⋅ rev $l;
 
-opaque symbol rev_idem {a} (l :𝕃 a) : π(rev (rev l) = l) ≔
+opaque symbol rev_idem [a] (l :𝕃 a) : π(rev (rev l) = l) ≔
 begin
-  assume a;
-  induction;
-  // case l = □
-  reflexivity;
-  // case l = ⸬
-  assume x l h; simplify; rewrite h; reflexivity;
+  assume a; induction
+  { reflexivity }
+  { assume x l h; simplify; rewrite h; reflexivity }
 end;
 
 rule rev (rev $l) ↪ $l;
 
-opaque symbol length_rev {a} (l : 𝕃 a) : π(length (rev l) = length l) ≔
+opaque symbol length_rev [a] (l : 𝕃 a) : π(length (rev l) = length l) ≔
 begin
-  assume a;
-  induction;
-  // case l = □
-  simplify; reflexivity;
-  // case l = ⸬
-  assume x l h; simplify; rewrite h; reflexivity;
+  assume a; induction
+  { simplify; reflexivity }
+  { assume x l h; simplify; rewrite h; reflexivity }
 end;
 
 rule length (rev $l) ↪ length $l;