From 9991f37bb5c204ee7607bdda1cc038847f4b1320 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Wed, 2 Jul 2025 16:02:51 +0200
Subject: [PATCH 1/2] replace some apply's by refine's

---
 List.lp | 296 ++++++++++++++++++++++++++++----------------------------
 Nat.lp  |  18 ++--
 Pos.lp  |   4 +-
 3 files changed, 159 insertions(+), 159 deletions(-)

diff --git a/List.lp b/List.lp
index 4e50bc0..58e5dba 100644
--- a/List.lp
+++ b/List.lp
@@ -249,7 +249,7 @@ with behead (_ ⸬ $l) ↪ $l;
 
 opaque symbol ⸬_inj [a] [x:τ a] [l y m] : π(x ⸬ l = y ⸬ m) → π(x = y ∧ l = m) ≔
 begin
-  assume a x l y m e; apply ∧ᵢ { apply feq (head x) e } { apply feq behead e }
+  assume a x l y m e; apply ∧ᵢ { refine feq (head x) e } { refine feq behead e }
 end;
 
 // boolean equality on lists
@@ -270,7 +270,7 @@ begin
     { simplify; assume y m i c; refine ⊥ₑ c }
   }
   { assume x l h; induction
-    { simplify; assume c; refine ⊥ₑ c; }
+    { simplify; assume c; refine ⊥ₑ c }
     { simplify; assume y m i c;
       apply feq2 (⸬) _ _
       { apply beq_correct; apply @andₑ₁ _ (eql beq l m) c}
@@ -284,9 +284,9 @@ opaque symbol eql_complete a (beq : τ a → τ a → 𝔹) :
   π(`∀ x, `∀ y, x = y ⇒ beq x y) → π(`∀ l, `∀ m, l = m ⇒ eql beq l m) ≔
 begin
   assume a beq beq_complete; induction
-  { assume m i; rewrite left i; apply ⊤ᵢ; }
+  { assume m i; rewrite left i; apply ⊤ᵢ }
   { assume x l h; induction
-    { assume j; apply ⸬≠□ j; }
+    { assume j; apply ⸬≠□ j }
     { assume y m i j; simplify;
       have j': π(x = y ∧ l = m) { apply ⸬_inj j };
       apply @istrue_and (beq x y) (eql beq l m); apply ∧ᵢ
@@ -306,8 +306,8 @@ with size (_ ⸬ $l) ↪ size $l +1;
 opaque symbol size0nil [a] (l:𝕃 a) : π (size l = 0) → π (l = □) ≔
 begin
   assume a; induction
-  { reflexivity; }
-  { assume e l h i; apply ⊥ₑ; apply s≠0 i; }
+  { reflexivity }
+  { assume e l h i; apply ⊥ₑ; apply s≠0 i }
 end;
 
 symbol nilp [a] l ≔ is0 (@size a l);
@@ -315,8 +315,8 @@ symbol nilp [a] l ≔ is0 (@size a l);
 opaque symbol size_behead [a] (l:𝕃 a) : π (size (behead l) = size l ∸1) ≔
 begin
   assume a; induction
-  { reflexivity; }
-  { assume e l h; reflexivity; }
+  { reflexivity }
+  { assume e l h; reflexivity }
 end;
 
 // concatenation
@@ -361,30 +361,30 @@ with ncons ($n +1) $x $l ↪ $x ⸬ ncons $n $x $l;
 opaque symbol size_ncons [a] n (x:τ a) l : π (size (ncons n x l) = n + size l) ≔
 begin
   assume a; induction
-  { reflexivity; }
-  { assume n h x l; simplify; apply feq (+1) (h x l); }
+  { reflexivity }
+  { assume n h x l; simplify; apply feq (+1) (h x l) }
 end;
 
 opaque symbol size_nseq [a] n (x:τ a) : π (size (nseq n x) = n) ≔
 begin
   assume a; induction
-  { reflexivity; }
-  { assume n h x; simplify; apply feq (+1) (h x); }
+  { reflexivity }
+  { assume n h x; simplify; apply feq (+1) (h x) }
 end;
 
 opaque symbol cat_nseq [a] n (x:τ a) l : π (nseq n x ++ l = ncons n x l) ≔
 begin
   assume a; induction
-  { reflexivity; }
-  { assume n h x l; simplify; rewrite h x l; reflexivity; }
+  { reflexivity }
+  { assume n h x l; simplify; rewrite h x l; reflexivity }
 end;
 
 opaque symbol nseqD [a] n1 n2 (x:τ a) :
   π (nseq (n1 + n2) x = nseq n1 x ++ nseq n2 x) ≔
 begin
   assume a; induction
-  { reflexivity; }
-  { assume n1 h n2 x; simplify; rewrite h n2; reflexivity; }
+  { reflexivity }
+  { assume n1 h n2 x; simplify; rewrite h n2; reflexivity }
 end;
 
 opaque symbol cats0 [a] (l:𝕃 a) : π(l ++ □ = l) ≔
@@ -392,9 +392,9 @@ begin
   assume a;
   induction
     // case l = □
-    { reflexivity; }
+    { reflexivity }
     // case l = x ⸬ l'
-    { assume x l' h; simplify; rewrite h; reflexivity; }
+    { assume x l' h; simplify; rewrite h; reflexivity }
 end;
 
 rule $m ++ □ ↪ $m;
@@ -404,9 +404,9 @@ begin
   assume a;
   induction
     // case l = □
-    { reflexivity; }
+    { reflexivity }
     // case l = x⸬l'
-    { assume x l' h m; simplify; rewrite h; reflexivity; }
+    { assume x l' h m; simplify; rewrite h; reflexivity }
 end;
 
 rule size ($l ++ $m) ↪ size $l + size $m;
@@ -416,9 +416,9 @@ begin
   assume a;
   induction
     // case l = □
-    { reflexivity; }
+    { reflexivity }
     // case l = x⸬l'
-    { assume x l' h m n; simplify; rewrite h; reflexivity; }
+    { assume x l' h m n; simplify; rewrite h; reflexivity }
 end;
 
 rule ($l ++ $m) ++ $n ↪ $l ++ ($m ++ $n);
@@ -427,8 +427,8 @@ opaque symbol cat_nilp [a] (l1 l2 : 𝕃 a) :
   π (nilp (l1 ++ l2) = (nilp l1 and nilp l2)) ≔
 begin
   assume a; induction
-  { reflexivity; }
-  { assume e l h l2; simplify; reflexivity; }
+  { reflexivity }
+  { assume e l h l2; simplify; reflexivity }
 end;
 
 // list reversal
@@ -443,9 +443,9 @@ begin
   assume a;
   induction
     // case l = □
-    { simplify; reflexivity; }
+    { simplify; reflexivity }
     // case l = ⸬
-    { assume x l h m; simplify; rewrite h; reflexivity; }
+    { assume x l h m; simplify; rewrite h; reflexivity }
 end;
 
 rule rev ($l ++ $m) ↪ rev $m ++ rev $l;
@@ -462,9 +462,9 @@ begin
   assume a;
   induction
     // case l = □
-    { simplify; reflexivity; }
+    { simplify; reflexivity }
     // case l = ⸬
-    { assume x l h; simplify; rewrite h; reflexivity; }
+    { assume x l h; simplify; rewrite h; reflexivity }
 end;
 
 // rcons
@@ -477,8 +477,8 @@ with rcons ($e ⸬ $l) $x ↪ $e ⸬ (rcons $l $x);
 opaque symbol cats1 [a] (l:𝕃 a) (z:τ a) : π (l ++ (z ⸬ □) = rcons l z) ≔
 begin
   assume a; induction
-  { reflexivity; }
-  { assume e l h z; simplify; rewrite h z; reflexivity; }
+  { reflexivity }
+  { assume e l h z; simplify; rewrite h z; reflexivity }
 end;
 
 opaque symbol rcons_cons [a] (x:τ a) (s:𝕃 a) (z:τ a) :
@@ -610,10 +610,10 @@ opaque symbol unzip1_zip [a b] (la:𝕃 a) (lb:𝕃 b) :
   π (size la ≤ size lb) → π (unzip1 (zip la lb) = la) ≔
 begin
   assume a b; induction
-  { reflexivity; }
+  { reflexivity }
   { assume ea la h; induction
-    { assume i; apply ⊥ₑ i; }
-    { assume eb lb i j; apply feq (λ l, ea ⸬ l) (h lb j); }
+    { assume i; apply ⊥ₑ i }
+    { assume eb lb i j; apply feq (λ l, ea ⸬ l) (h lb j) }
   }
 end;
 
@@ -622,11 +622,11 @@ opaque symbol unzip2_zip [a b] (la:𝕃 a) (lb:𝕃 b) :
 begin
   assume a b; induction
   { assume lb h;
-     have t:π (size lb = 0) { apply ≤0 (size lb) h; };
-     symmetry; apply size0nil lb t; }
+     have t:π (size lb = 0) { apply ≤0 (size lb) h };
+     symmetry; apply size0nil lb t }
   { assume ea la h; induction
-    { reflexivity; }
-    { assume eb lb i j; apply feq (λ l, eb ⸬ l) (h lb j); }
+    { reflexivity }
+    { assume eb lb i j; apply feq (λ l, eb ⸬ l) (h lb j) }
   }
 end;
 
@@ -634,10 +634,10 @@ opaque symbol size1_zip [a b] (la:𝕃 a) (lb:𝕃 b) :
   π (size la ≤ size lb) → π (size (zip la lb) = size la) ≔
 begin
   assume a b; induction
-  { reflexivity; }
+  { reflexivity }
   { assume ea la h; induction
-    { assume i; apply ⊥ₑ i; }
-    { assume eb lb i j; apply feq (+1) (h lb j); }
+    { assume i; apply ⊥ₑ i }
+    { assume eb lb i j; apply feq (+1) (h lb j) }
   }
 end;
 
@@ -645,10 +645,10 @@ opaque symbol size2_zip [a b] (la:𝕃 a) (lb:𝕃 b) :
   π (size lb ≤ size la) → π (size (zip la lb) = size lb) ≔
 begin
   assume a b; induction
-  { assume lb h; symmetry; apply ≤0 (size lb) h; }
+  { assume lb h; symmetry; apply ≤0 (size lb) h }
   { assume ea la h; induction
-    { reflexivity; }
-    { assume eb lb i j; apply feq (+1) (h lb j); }
+    { reflexivity }
+    { assume eb lb i j; apply feq (+1) (h lb j) }
   }
 end;
 
@@ -658,8 +658,8 @@ begin
   assume a b; induction
   { reflexivity }
   { assume ea la h; induction
-    { reflexivity; }
-    { assume eb lb i; simplify; apply feq (+1) (h lb); }
+    { reflexivity }
+    { assume eb lb i; simplify; apply feq (+1) (h lb) }
   }
 end;
 
@@ -672,14 +672,14 @@ opaque symbol seq_ind2 [a b] (p:𝕃 a → 𝕃 b → Prop) :
 begin
   assume a b p p0 pH; induction
   { induction
-    { assume h; apply p0; }
+    { assume h; apply p0 }
     { assume eb lb h1 h2; apply ⊥ₑ; apply s≠0 [size lb]; symmetry; apply h2 }
   }
   { assume ea la h; induction
-    { assume i; apply ⊥ₑ (s≠0 i); }
+    { assume i; apply ⊥ₑ (s≠0 i) }
     { assume eb lb i j;
-      have t:π (size la = size lb) { apply +1_inj j; };
-      apply pH la lb ea eb t (h lb t); }
+      have t:π (size la = size lb) { apply +1_inj j };
+      apply pH la lb ea eb t (h lb t) }
   }
 end;
 
@@ -699,13 +699,13 @@ opaque symbol nth_zip [a b] (x:τ a) (y:τ b) la lb i: π(size la = size lb) →
 begin
   assume a b x y; induction
   { assume lb i h;
-    have t: π (lb = □) { apply size0nil lb; symmetry; apply h; };
-    rewrite t; reflexivity; }
+    have t: π (lb = □) { apply size0nil lb; symmetry; apply h };
+    rewrite t; reflexivity }
   { assume ea la h; induction
-    { assume i j; apply ⊥ₑ (s≠0 j); }
+    { assume i j; apply ⊥ₑ (s≠0 j) }
     { assume eb lb k; induction
-      { assume m; reflexivity; }
-      { assume i m n; apply h lb i _; apply +1_inj n; }
+      { assume m; reflexivity }
+      { assume i m n; refine h lb i _; apply +1_inj n }
     }
   }
 end;
@@ -750,16 +750,16 @@ begin
   }
   {
     assume n h; induction
-    { reflexivity; }
-    { assume e l i; simplify; refine h l; }
+    { reflexivity }
+    { assume e l i; simplify; refine h l }
   }
 end;
 
 opaque symbol drop_size [a] (l:𝕃 a) : π (drop (size l) l = □) ≔
 begin
   assume a; induction
-  { reflexivity; }
-  { assume e l h; simplify; apply h; }
+  { reflexivity }
+  { assume e l h; simplify; apply h }
 end;
 
 opaque symbol drop_cons [a] (e:τ a) l n : π (drop (n +1) (e ⸬ l) = drop n l) ≔
@@ -770,10 +770,10 @@ end;
 opaque symbol size_drop [a] (l:𝕃 a) n : π (size (drop n l) = size l - n) ≔
 begin
   assume a; induction
-  { reflexivity; }
+  { reflexivity }
   { assume e l h; simplify; induction
-    { reflexivity; }
-    { assume n i; simplify; apply h n; } 
+    { reflexivity }
+    { assume n i; simplify; apply h n } 
   }
 end;
 
@@ -781,12 +781,12 @@ opaque symbol size_cons [a] (e:τ a) n l : π (size l = n ⇔ size (e ⸬ l) = n
 begin
   assume a e n l; apply ∧ᵢ {
     generalize n; induction
-    { assume l h; simplify; rewrite h; reflexivity; }
+    { assume l h; simplify; rewrite h; reflexivity }
     { assume n h l i; simplify; apply feq (+1) i;}
   } {
     generalize n; induction
     { assume l i; apply +1_inj i;}
-    { assume n h l i; apply +1_inj i; }
+    { assume n h l i; apply +1_inj i }
   };
 end;
 
@@ -795,10 +795,10 @@ opaque symbol drop_size_cat [a] n (l1 l2:𝕃 a) :
 begin
   assume a; induction
   { assume l1 l2 h; simplify;
-    have t:π (l1 = □) { apply size0nil l1 h }; rewrite t; reflexivity; }
+    have t:π (l1 = □) { apply size0nil l1 h }; rewrite t; reflexivity }
   { assume n h; induction
-    { assume l2 i; apply ⊥ₑ; apply s≠0 [n]; symmetry; apply i; }
-    { assume e l1 i l2 j; apply h l1 l2; apply +1_inj j; }
+    { assume l2 i; apply ⊥ₑ; apply s≠0 [n]; symmetry; apply i }
+    { assume e l1 i l2 j; apply h l1 l2; apply +1_inj j }
   }
 end;
 
@@ -806,10 +806,10 @@ opaque symbol drop_drop [a] (l:𝕃 a) n1 n2 :
   π (drop n1 (drop n2 l) = drop (n1 + n2) l) ≔
 begin
   assume a; induction
-  { reflexivity; }
+  { reflexivity }
   { assume e l h n1; induction
-    { reflexivity; }
-    { assume n2 i; simplify; apply h n1 n2; }
+    { reflexivity }
+    { assume n2 i; simplify; apply h n1 n2 }
   }
 end;
 
@@ -838,27 +838,27 @@ end;
 opaque symbol take_size [a] (l: 𝕃 a) : π (take (size l) l = l) ≔
 begin
   assume a; induction
-  { reflexivity; }
-  { assume e l h; simplify; rewrite h; reflexivity; }
+  { reflexivity }
+  { assume e l h; simplify; rewrite h; reflexivity }
 end;
 
 opaque symbol take_oversize [a] n (l:𝕃 a) : π (size l ≤ n) → π (take n l = l) ≔
 begin
   assume a; induction
-  { assume l h; simplify; symmetry; apply size0nil l; apply ≤0 (size l) h; }
+  { assume l h; simplify; symmetry; apply size0nil l; apply ≤0 (size l) h }
   { assume n h; induction
-    { reflexivity; }
-    { assume e l i; simplify; assume j; rewrite h l j; reflexivity; }
+    { reflexivity }
+    { assume e l i; simplify; assume j; rewrite h l j; reflexivity }
   }
 end;
 
 opaque symbol cat_take_drop [a] n (l:𝕃 a) : π (take n l ++ drop n l = l) ≔
 begin
   assume a; induction
-  { reflexivity; }
+  { reflexivity }
   { assume n h; induction
-    { reflexivity; }
-    { assume e l i; simplify; rewrite h l; reflexivity; }
+    { reflexivity }
+    { assume e l i; simplify; rewrite h l; reflexivity }
   }
 end;
 
@@ -866,10 +866,10 @@ opaque symbol size_takel [a] n (l:𝕃 a) :
   π (n ≤ size l) → π (size (take n l) = n) ≔
 begin
   assume a; induction
-  { reflexivity; }
+  { reflexivity }
   { assume n h; induction
-    { simplify; assume i; apply ⊥ₑ i; }
-    { assume e l i; simplify; assume j; apply feq (+1); apply h l j; }
+    { simplify; assume i; apply ⊥ₑ i }
+    { assume e l i; simplify; assume j; apply feq (+1); apply h l j }
   }
 end;
 
@@ -882,10 +882,10 @@ opaque symbol size_take_min [a] n (l:𝕃 a) :
   π (size (take n l) = min n (size l)) ≔
 begin
   assume a; induction
-  { reflexivity; }
+  { reflexivity }
   { assume n h; induction
-    { reflexivity; }
-    { assume e l i; simplify; apply feq (+1) (h l); }
+    { reflexivity }
+    { assume e l i; simplify; apply feq (+1) (h l) }
   }
 end;
 
@@ -893,9 +893,9 @@ opaque symbol take_size_cat [a] n (l1 l2:𝕃 a) :
   π (size l1 = n) → π (take n (l1 ++ l2) = l1) ≔
 begin
   assume a; induction
-  { assume l1 l2 h; simplify; symmetry; apply size0nil l1 h; }
+  { assume l1 l2 h; simplify; symmetry; apply size0nil l1 h }
   { assume n h; induction
-    { assume l2 i; apply ⊥ₑ; apply s≠0 [n]; symmetry; apply i; }
+    { assume l2 i; apply ⊥ₑ; apply s≠0 [n]; symmetry; apply i }
     { assume e1 l1 i l2 j; simplify; apply feq (λ l, e1 ⸬ l);
       apply h l1 l2; apply ∧ₑ₂ (size_cons e1 n l1) j; 
     }
@@ -906,10 +906,10 @@ opaque symbol takel_cat [a] (l1 l2:𝕃 a) n :
   π (n ≤ size l1) → π (take n (l1 ++ l2) = take n l1) ≔
 begin
   assume a; induction
-  { assume l2 n h; have t:π (n = 0) { apply ≤0 n h }; rewrite t; reflexivity; }
+  { assume l2 n h; have t:π (n = 0) { apply ≤0 n h }; rewrite t; reflexivity }
   { assume e1 l1 h l2; induction
-    { reflexivity; }
-    { assume n i j; apply feq (λ l:𝕃 a, e1 ⸬ l); apply h l2 n j; }
+    { reflexivity }
+    { assume n i j; apply feq (λ l:𝕃 a, e1 ⸬ l); apply h l2 n j }
   }
 end;
 
@@ -918,18 +918,18 @@ opaque symbol take_drop [a] m n (l:𝕃 a):
 begin
   assume a; induction
   { induction
-    { reflexivity; }
+    { reflexivity }
     { assume m h; induction
-      { reflexivity; }
+      { reflexivity }
       { assume e l i; simplify; rewrite left .[m in take m l] add0n m;
-        rewrite left h l; reflexivity; }
+        rewrite left h l; reflexivity }
     }
   }
   { assume n h; induction
-    { reflexivity; }
+    { reflexivity }
     { assume m i; induction
-      { reflexivity; }
-      { assume e l j; simplify; apply i l; }
+      { reflexivity }
+      { assume e l j; refine i l }
     }
   }
 end;
@@ -938,13 +938,13 @@ opaque symbol takeD [a] m n (l:𝕃 a) :
   π (take (m + n) l = take m l ++ take n (drop m l)) ≔
 begin
   assume a; induction
-  { reflexivity; }
+  { reflexivity }
   { assume m h; induction
-    { reflexivity; }
+    { reflexivity }
     { assume n i; induction
-      { reflexivity; }
+      { reflexivity }
       { assume e l j; simplify; apply feq (λ l:𝕃 a, e ⸬ l);
-        rewrite left addnS; apply h (n +1) l; }
+        rewrite left addnS; apply h (n +1) l }
     }
   }
 end;
@@ -953,12 +953,12 @@ opaque symbol takeC [a] (l:𝕃 a) i j:
   π (take i (take j l) = take j (take i l)) ≔
 begin
   assume a; induction
-  { reflexivity; }
+  { reflexivity }
   { assume e l h; induction
-    { reflexivity; }
+    { reflexivity }
     { assume i h2; induction
-      { reflexivity; }
-      { assume j h3; simplify; rewrite h i j; reflexivity; }
+      { reflexivity }
+      { assume j h3; simplify; rewrite h i j; reflexivity }
     }
   }
 end;
@@ -1010,12 +1010,12 @@ opaque symbol take_take [a] n m :
   π (n ≤ m) → π (`∀ l:𝕃 a, take n (take m l) = take n l) ≔
 begin
   assume a; induction
-  { reflexivity; }
+  { reflexivity }
   { assume n h; induction
-    { assume i; apply ⊥ₑ i; }
+    { assume i; apply ⊥ₑ i }
     { assume m i j; induction
-      { reflexivity; }
-      { assume e l k; simplify; apply feq (λ l:𝕃 a, e ⸬ l) (h m j l); }
+      { reflexivity }
+      { assume e l k; simplify; apply feq (λ l:𝕃 a, e ⸬ l) (h m j l) }
     }
   }
 end;
@@ -1057,8 +1057,8 @@ opaque symbol in_cons [a] beq (x y:τ a) l :
   π (∈ beq x (y ⸬ l) = beq x y or ∈ beq x l) ≔
 begin
   assume a beq x y; induction
-  { reflexivity; }
-  { assume e l h; reflexivity; }
+  { reflexivity }
+  { assume e l h; reflexivity }
 end;
 
 opaque symbol in_nil [a] beq (x:τ a) : π (∈ beq x □ = false) ≔
@@ -1075,9 +1075,9 @@ opaque symbol mem_cat [a] beq (x:τ a) l1 l2 :
   π (∈ beq x (l1 ++ l2) = ∈ beq x l1 or ∈ beq x l2) ≔
 begin
   assume a beq x; induction
-  { reflexivity; }
+  { reflexivity }
   { assume e1 l1 h; simplify; assume l2; rewrite h l2; rewrite orA;
-    reflexivity; }
+    reflexivity }
 end;
 
 opaque symbol mem_head [a] beq (x:τ a) l :
@@ -1094,11 +1094,11 @@ begin
     {assume n0 l h1 h2;
     have H0: π (beq n n0) →  π (beq n m or (beq n n0 or ∈ beq n l))
       {assume h3;
-      refine orᵢ₂ (beq n m) [beq n n0 or ∈ beq n l] (orᵢ₁ [beq n n0] (∈ beq n l) h3)};
+      refine orᵢ₂ (beq n m) (orᵢ₁ [beq n n0] (∈ beq n l) h3)};
     have H1: π (∈ beq n l) →  π (beq n m or (beq n n0 or ∈ beq n l))
       {assume h3;
-      refine orᵢ₂ (beq n m) [beq n n0 or ∈ beq n l] (orᵢ₂ (beq n n0) [∈ beq n l] h3)};
-    refine orₑ [beq n n0] [∈ beq n l] (beq n m or (beq n n0 or ∈ beq n l)) h2 H0 H1}
+      refine orᵢ₂ (beq n m) (orᵢ₂ (beq n n0) [∈ beq n l] h3)};
+    refine orₑ (beq n m or (beq n n0 or ∈ beq n l)) h2 H0 H1}
 end;
 
 opaque symbol mem_take [a] beq n l (x:τ a) :
@@ -1106,7 +1106,7 @@ opaque symbol mem_take [a] beq n l (x:τ a) :
 begin
   assume a beq n l x h; rewrite left cat_take_drop n l;
   rewrite mem_cat beq x (take n l) (drop n l);
-  refine @orᵢ₁ (∈ beq x (take n l)) (∈ beq x (drop n l)) h;
+  refine orᵢ₁ (∈ beq x (drop n l)) h;
 end;
 
 opaque symbol mem_drop [a] beq n l (x:τ a) :
@@ -1114,7 +1114,7 @@ opaque symbol mem_drop [a] beq n l (x:τ a) :
 begin
   assume a beq n l x h; rewrite left cat_take_drop n l;
   rewrite mem_cat beq x (take n l) (drop n l);
-  refine @orᵢ₂ (∈ beq x (take n l)) (∈ beq x (drop n l)) h;
+  refine orᵢ₂ (∈ beq x (take n l)) h;
 end;
 
 opaque symbol mem_rcons_left [a] beq (n m : τ a) (l : 𝕃 a) :
@@ -1130,7 +1130,7 @@ begin
           have H1: π (∈ beq n l) →  π (beq n n0 or ∈ beq n (rcons l m))
             { assume h3;
               refine (orᵢ₂ (beq n n0) [∈ beq n (rcons l m)] (h1 h3)) };
-          refine orₑ [beq n n0] [∈ beq n l] (beq n n0 or ∈ beq n (rcons l m)) h2 H0 H1 }
+          refine orₑ (beq n n0 or ∈ beq n (rcons l m)) h2 H0 H1 }
 end;
 
 opaque symbol 0∈indexes⸬ [a] (x : τ a) (l: 𝕃 a) :
@@ -1153,7 +1153,7 @@ begin
       { assume k h1 m; simplify; assume h2;
         refine orₑ [eqn n m] [∈ eqn n (iota (m +1) k)] (eqn n m or ∈ eqn (n +1) (iota ((m +1) +1) k)) h2 _ _
           { assume h3;
-            refine orᵢ₁ [eqn n m] (∈ eqn (n +1) (iota ((m +1) +1) k)) h3 }
+            refine orᵢ₁ (∈ eqn (n +1) (iota ((m +1) +1) k)) h3 }
           { assume h3;
             refine orᵢ₂ (eqn n m) [∈ eqn (n +1) (iota ((m +1) +1) k)] _;
             refine h1 (m +1) _; refine h3
@@ -1170,8 +1170,8 @@ begin
   { simplify; assume x h; refine h }
   { assume x l h y; simplify; assume i;
     refine orₑ [eqn n 0] [∈ eqn n (iota 1 (size l))] _ i _ _
-      { assume j; apply orᵢ₁ [eqn n 0] (∈ eqn (n +1) (iota 2 (size l))) j }
-      { assume j; apply orᵢ₂ (eqn n 0) [∈ eqn (n +1) (iota 2 (size l))] _;
+      { assume j; refine orᵢ₁ (∈ eqn (n +1) (iota 2 (size l))) j }
+      { assume j; refine orᵢ₂ (eqn n 0) [∈ eqn (n +1) (iota 2 (size l))] _;
         refine +1∈iota+1 n 1 (size l) j;
       }
   }
@@ -1190,7 +1190,7 @@ assert ⊢ index eqn 26 (42 ⸬ 2 ⸬ 51 ⸬ 3 ⸬ □) ≡ 4;
 opaque symbol index_size [a] beq (x:τ a) l : π (index beq x l ≤ size l) ≔
 begin
   assume a beq x; induction
-  { apply ⊤ᵢ; }
+  { apply ⊤ᵢ }
   { assume e l h; simplify;
     refine ind_𝔹 (λ b, istrue (if b 0 (index beq x l +1) ≤ size l +1)) _ _ (beq x e) {
       apply ⊤ᵢ;
@@ -1239,7 +1239,7 @@ assert ⊢ find (λ x, eqn (x + 1) 3) (42 ⸬ 4 ⸬ 51 ⸬ 3 ⸬ □) ≡ 4;
 opaque symbol find_size [a] (p:τ a → 𝔹) l : π (find p l ≤ size l) ≔
 begin
   assume a p; induction
-  { apply ⊤ᵢ; }
+  { apply ⊤ᵢ }
   { assume e l h;
     refine ind_𝔹 (λ x, istrue (if x 0 (find p l +1) ≤ size l +1)) _ _ (p e) {
       apply ⊤ᵢ;
@@ -1262,7 +1262,7 @@ assert ⊢ count (λ x, eqn (x + 1) 3) (2 ⸬ 2 ⸬ 2 ⸬ 2 ⸬ □) ≡ 4;
 opaque symbol count_size [a] (p:τ a → 𝔹) l : π(count p l ≤ size l) ≔
 begin
   assume a p; induction
-  { apply ⊤ᵢ; }
+  { apply ⊤ᵢ }
   { assume e l h; simplify;
     refine ind_𝔹 (λ x, istrue (if x (count p l +1) (count p l) ≤ size l +1)) _ _ (p e) {
       simplify; apply h;
@@ -1377,7 +1377,7 @@ opaque symbol size_filter [a] (p:τ a → 𝔹) l :
   π (size (filter p l) = count p l) ≔
 begin
   assume a p; induction
-  { reflexivity; }
+  { reflexivity }
   { assume e l h; simplify;
     refine ind_𝔹 (λ x, size (if x (e ⸬ filter p l) (filter p l)) = (if x (count p l +1) (count p l))) _ _ (p e) {
       simplify; apply feq (+1) h;
@@ -1391,7 +1391,7 @@ opaque symbol filter_cat [a] (p:τ a → 𝔹) l1 l2 :
   π (filter p (l1 ++ l2) = filter p l1 ++ filter p l2) ≔
 begin
   assume a p; induction
-  { reflexivity; }
+  { reflexivity }
   { assume e1 l1 h l2; simplify;
     refine ind_𝔹 (λ x, if x (e1 ⸬ filter p (l1 ++ l2)) (filter p (l1 ++ l2)) = if x (e1 ⸬ filter p l1) (filter p l1) ++ filter p l2) _ _ (p e1) {
       simplify; rewrite h l2; reflexivity;
@@ -1405,7 +1405,7 @@ opaque symbol filter_rev [a] (p:τ a → 𝔹) l :
   π (filter p (rev l) = rev (filter p l)) ≔
 begin
   assume a p; induction
-  { reflexivity; }
+  { reflexivity }
   { assume e l h; simplify; rewrite filter_cat p (rev l) (e ⸬ □); simplify;
     refine ind_𝔹 (λ b:𝔹, (filter p (rev l) ++ (if b (e ⸬ □) □) = rev (if b (e ⸬ filter p l) (filter p l)))) _ _ (p e) {
       simplify; rewrite h; reflexivity;
@@ -1442,7 +1442,7 @@ assert ⊢ undup eqn (42 ⸬ 2 ⸬ 51 ⸬ 3 ⸬ 2 ⸬ 3 ⸬ □) ≡ 42 ⸬ 51 
 opaque symbol size_undup [a] beq (l:𝕃 a) : π (size (undup beq l) ≤ size l) ≔
 begin
   assume a beq; induction
-  { apply ⊤ᵢ; }
+  { apply ⊤ᵢ }
   { assume e l h; simplify;
     refine ind_𝔹 (λ x, istrue (size (if x (undup beq l) (e ⸬ undup beq l)) ≤ size l +1)) _ _ (∈ beq e (undup beq l)) {
       simplify;
@@ -1456,7 +1456,7 @@ end;
 opaque symbol undup_uniq [a] beq (l:𝕃 a) : π (uniq beq (undup beq l)) ≔
 begin
   assume a beq; induction
-  { apply ⊤ᵢ; }
+  { apply ⊤ᵢ }
   { assume e l h; simplify;
     refine ind_𝔹_eq (λ b, (istrue(uniq beq (if b (undup beq l) (e ⸬ (undup beq l)))))) (∈ beq e (undup beq l)) _ _ {
       assume i; rewrite i; simplify; apply h;
@@ -1495,57 +1495,57 @@ opaque symbol map_cat [a b] (f:τ a → τ b) l1 l2 :
   π (map f (l1 ++ l2) = map f l1 ++ map f l2) ≔
 begin
   assume a b f; induction
-  { reflexivity; }
-  { assume e1 l1 h l2; simplify; rewrite h l2; reflexivity; }
+  { reflexivity }
+  { assume e1 l1 h l2; simplify; rewrite h l2; reflexivity }
 end;
 
 opaque symbol size_map [a b] (f:τ a → τ b) l : π (size (map f l) = size l) ≔
 begin
   assume a b f; induction
-  { reflexivity; }
-  { assume e l h; simplify; apply feq (+1) h; }
+  { reflexivity }
+  { assume e l h; simplify; apply feq (+1) h }
 end;
 
 opaque symbol behead_map [a b] (f:τ a → τ b) l :
   π (behead (map f l) = map f (behead l)) ≔
 begin
   assume a b f; induction
-  { reflexivity; }
-  { assume e l h; reflexivity; }
+  { reflexivity }
+  { assume e l h; reflexivity }
 end;
 
 opaque symbol map_rcons [a b] (f:τ a → τ b) l e :
   π (map f (rcons l e) = rcons (map f l) (f e)) ≔
 begin
   assume a b f; induction
-  { reflexivity; }
-  { assume x l h e; simplify; rewrite h e; reflexivity; }
+  { reflexivity }
+  { assume x l h e; simplify; rewrite h e; reflexivity }
 end;
 
 opaque symbol last_map [a b] (f:τ a → τ b) l x :
   π (last (f x) (map f l) = f (last x l)) ≔
 begin
   assume a b f; induction
-  { reflexivity; }
-  { assume e l h x; simplify; rewrite h e; reflexivity; }
+  { reflexivity }
+  { assume e l h x; simplify; rewrite h e; reflexivity }
 end;
 
 opaque symbol belast_map [a b] (f:τ a → τ b) l x :
   π (belast (f x) (map f l) = map f (belast x l)) ≔
 begin
   assume a b f; induction
-  { reflexivity; }
-  { assume e l h x; simplify; rewrite h e; reflexivity; }
+  { reflexivity }
+  { assume e l h x; simplify; rewrite h e; reflexivity }
 end;
 
 opaque symbol map_take [a b] (f:τ a → τ b) n l :
   π (map f (take n l) = take n (map f l)) ≔
 begin
   assume a b f; induction
-  { reflexivity; }
+  { reflexivity }
   { assume n h; induction
-    { reflexivity; }
-    { assume e l i; simplify; rewrite h l; reflexivity; } 
+    { reflexivity }
+    { assume e l i; simplify; rewrite h l; reflexivity } 
   }
 end;
 
@@ -1553,10 +1553,10 @@ opaque symbol map_drop [a b] (f:τ a → τ b) n l :
   π (map f (drop n l) = drop n (map f l)) ≔
 begin
   assume a b f; induction
-  { reflexivity; }
+  { reflexivity }
   { assume n h; induction
-    { reflexivity; }
-    { assume e l i; simplify; rewrite h l; reflexivity; } 
+    { reflexivity }
+    { assume e l i; simplify; rewrite h l; reflexivity } 
   }
 end;
 
@@ -1580,9 +1580,9 @@ opaque symbol map_rev [a b] (f:τ a → τ b) l :
   π (map f (rev l) = rev (map f l)) ≔
 begin
   assume a b f; induction
-  { reflexivity; }
+  { reflexivity }
   { assume e l h; simplify; rewrite map_cat f (rev l) (e ⸬ □); rewrite h;
-    reflexivity; }
+    reflexivity }
 end;
 
 opaque symbol inj_map [a b] (f:τ a → τ b) :
@@ -1591,7 +1591,7 @@ opaque symbol inj_map [a b] (f:τ a → τ b) :
 begin
   assume a b f h; induction
   { induction
-    { reflexivity; }
+    { reflexivity }
     { simplify; assume e l i j; apply ⊥ₑ (□≠⸬ j) }
   }
   { assume e1 l1 i; induction
diff --git a/Nat.lp b/Nat.lp
index 56b84a3..005d5f4 100644
--- a/Nat.lp
+++ b/Nat.lp
@@ -133,7 +133,7 @@ with ($x +1) ∸1 ↪ $x;
 
 opaque symbol +1_inj [x y] : π (x +1 = y +1) → π (x = y) ≔
 begin
-  assume x y h; apply feq (∸1) h
+  assume x y h; refine feq (∸1) h
 end;
 
 // boolean equality on ℕ
@@ -329,7 +329,7 @@ begin
   }
   { assume x h; induction
     { refine s≠0 }
-    { assume y i j; apply h y; apply +1_inj; apply +1_inj; apply j }
+    { assume y i j; apply h y; apply +1_inj; apply +1_inj; refine j }
   }
 end;
 
@@ -847,11 +847,11 @@ opaque symbol leq_add2l p m n : π (istrue (p + m ≤ p + n) ⇔ istrue (m ≤ n
 begin
   assume p m n; apply ∧ᵢ {
     generalize p; induction
-    { assume m n h; apply h }
+    { assume m n h; refine h }
     { assume p h m n i; apply h m n i }
   } {
     generalize p; induction
-    { assume m n h; apply h }
+    { assume m n h; refine h }
     { assume p h m n i; apply h m n i }
   }; 
 end;
@@ -954,7 +954,7 @@ begin
         have t: π (istrue (m < n)) { apply h n j };
         have u: π (istrue (m +1 < n +1))
                   { refine ∧ₑ₂ (ltn_add2r (_0 +1) m n) t };
-        rewrite left addn1 m; rewrite left addn1 n; apply u;
+        rewrite left addn1 m; rewrite left addn1 n; refine u;
       }
     }
   } {
@@ -983,12 +983,12 @@ begin
   assume m n p; apply ∧ᵢ
   { assume h;
     have t: π (((m - (n + p)) = _0)) → π (istrue (m ≤ (n + p)))
-      { apply ∧ₑ₁ (subn_eq0 m (n + p)) };
+      { refine ∧ₑ₁ (subn_eq0 m (n + p)) };
     apply t; rewrite subnDA; apply ∧ₑ₂ (subn_eq0 (m - n) p) h;
   }
   { assume h;
     have t: π (((m - n) - p) = _0) → π (istrue ((m - n) ≤ p))
-      { apply ∧ₑ₁ (subn_eq0 (m - n) p) };
+      { refine ∧ₑ₁ (subn_eq0 (m - n) p) };
     apply t; rewrite left subnDA; apply ∧ₑ₂ (subn_eq0 m (n + p)) h;
   };
 end;
@@ -1008,8 +1008,8 @@ begin
   induction
   { assume n; apply eq_refl n }
   { assume m h; induction
-    { apply eq_refl (m +1) }
-    { assume n i; simplify; apply feq (+1); apply h n }
+    { reflexivity }
+    { assume n i; apply feq (+1); apply h n }
   }
 end;
 
diff --git a/Pos.lp b/Pos.lp
index 1360c58..43ec495 100644
--- a/Pos.lp
+++ b/Pos.lp
@@ -71,7 +71,7 @@ with projO H ↪ H;
 
 opaque symbol O_inj p q : π(O p = O q) → π(p = q) ≔
 begin
-  assume p q h; apply feq projO h
+  assume p q h; refine feq projO h
 end;
 
 symbol projI : ℙ → ℙ;
@@ -82,7 +82,7 @@ with projI H ↪ H;
 
 opaque symbol I_inj p q : π(I p = I q) → π(p = q) ≔
 begin
-  assume p q h; apply feq projI h
+  assume p q h; refine feq projI h
 end;
 
 // Successor function

From 328372767756f05c310aef271282db93c9cf8978 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Wed, 2 Jul 2025 19:44:42 +0200
Subject: [PATCH 2/2] wip

---
 Z.lp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Z.lp b/Z.lp
index e8ffc36..c466493 100644
--- a/Z.lp
+++ b/Z.lp
@@ -559,7 +559,7 @@ begin
      induction
       { assume h1 h2; refine λ x, x;   }
       { assume y h h'; refine λ x, x }
-      { simplify; assume y h f; apply ⊥ₑ; refine f ⊤ᵢ } }
+      { simplify; assume y h f; refine ⊥ₑ _; refine f ⊤ᵢ } }
   { assume x y f h; apply ⊥ₑ; refine f ⊤ᵢ }
 end;