From 7e2d09f922ec3333b4fe578c9c7fae39d01e60a1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Tue, 19 Nov 2024 13:30:27 +0100
Subject: [PATCH 1/2] some cleaning

---
 Bool.lp |  5 ++---
 List.lp | 40 ++++++++++------------------------------
 Nat.lp  |  2 +-
 3 files changed, 13 insertions(+), 34 deletions(-)

diff --git a/Bool.lp b/Bool.lp
index 37b2ba6..8d01af4 100644
--- a/Bool.lp
+++ b/Bool.lp
@@ -27,7 +27,7 @@ end;
 
 // non confusion of constructors
 
-symbol istrue : 𝔹 → Prop;
+injective symbol istrue : 𝔹 → Prop;
 
 rule istrue true ↪ ⊤
 with istrue false ↪ ⊥;
@@ -136,8 +136,7 @@ end;
 
 opaque symbol andᵢ [p q] : π(istrue p) → π(istrue q) → π(istrue (p and q)) ≔
 begin
-  assume p q h i; //FIXME: apply istrue_and fails
-  apply @istrue_and p q; apply ∧ᵢ h i;
+  assume p q h i; apply @istrue_and p q; apply ∧ᵢ h i;
 end;
 
 opaque symbol andₑ₁ [p q] : π (istrue (p and q)) → π (istrue p) ≔
diff --git a/List.lp b/List.lp
index 007411d..f12ea5c 100644
--- a/List.lp
+++ b/List.lp
@@ -225,8 +225,7 @@ end;
 
 opaque symbol □≠⸬ [a] [x:τ a] [l] : π (□ ≠ x ⸬ l) ≔
 begin
-  assume a x l h; /*FIXME:apply ⸬≠□ fails*/ refine @⸬≠□ a x l _;
-  symmetry; apply h
+  assume a x l h; refine @⸬≠□ a x l _; symmetry; apply h
 end;
 
 // head
@@ -270,12 +269,9 @@ begin
   { assume x l h; induction
     { simplify; assume c; refine ⊥ₑ c; }
     { simplify; assume y m i c;
-      //FIXME: apply feq2 (⸬) fails
-      refine feq2 (⸬) _ _
-      { apply beq_correct; //FIXME: apply andₑ₁ c fails
-        apply @andₑ₁ (beq x y) (eql beq l m) c}
-      { apply h; //FIXME: apply andₑ₂ c fails
-        refine @andₑ₂ (beq x y) (eql beq l m) c
+      apply feq2 (⸬) _ _
+      { apply beq_correct; apply @andₑ₁ _ (eql beq l m) c}
+      { apply h; refine @andₑ₂ (beq x y) _ c
       } 
     }
   }
@@ -284,17 +280,15 @@ end;
 opaque symbol eql_complete a beq: π(`∀ x:τ a, `∀ y, x = y ⇒ istrue(beq x y)) →
   π(`∀ l, `∀ m, l = m ⇒ istrue(eql beq l m)) ≔
 begin
-  simplify; //FIXME: remove
   assume a beq beq_complete; induction
   { assume m i; rewrite left i; apply ⊤ᵢ; }
-  { simplify /*FIXME*/; assume x l h; induction
+  { assume x l h; induction
     { 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) /*FIXME*/; apply ∧ᵢ
+      apply @istrue_and (beq x y) (eql beq l m); apply ∧ᵢ
       { apply beq_complete x y; apply ∧ₑ₁ j' }
-      { //FIXME: apply h fails
-        refine h m _; apply ∧ₑ₂ j' }
+      { apply h m; apply ∧ₑ₂ j' }
     }
   }
 end;
@@ -457,15 +451,9 @@ opaque symbol rev_idem [a] (l :𝕃 a) : π(rev (rev l) = l) ≔
 begin
   assume a; induction
   { reflexivity }
-  { assume x l h;
-    /*FIXME: if no rule rev_concat, rewrite rev_concat fails:
-      Uncaught [File "src/handle/rewrite.ml", line 166
-    rewrite @rev_concat a;*/
-    simplify; rewrite h; reflexivity }
+  { assume x l h; simplify; rewrite h; reflexivity }
 end;
 
-//rule rev (rev $l) ↪ $l; creates confluence problems
-
 opaque symbol size_rev [a] (l : 𝕃 a) : π(size (rev l) = size l) ≔
 begin
   assume a;
@@ -476,8 +464,6 @@ begin
     { assume x l h; simplify; rewrite h; reflexivity; }
 end;
 
-//rule size (rev $l) ↪ size $l; // confluence modulo C
-
 // rcons
 
 symbol rcons [a] : 𝕃 a → τ a → 𝕃 a;
@@ -756,8 +742,6 @@ begin
   { assume e l h; simplify; apply h; }
 end;
 
-//rule drop (size $l) $l ↪ □;
-
 opaque symbol drop_cons [a] (e:τ a) l n : π (drop (n +1) (e ⸬ l) = drop n l) ≔
 begin
   assume a e l n; reflexivity;
@@ -992,10 +976,7 @@ end;
 
 opaque symbol rot_size [a] (l:𝕃 a) : π (rot (size l) l = l) ≔
 begin
-  assume a l; simplify; rewrite take_size l;
-  /*FIXME: Uncaught [File "src/core/infer.ml", line 101
-  rewrite @drop_size;*/
-  rewrite @drop_size a; reflexivity;
+  assume a l; simplify; rewrite take_size l; rewrite @drop_size a; reflexivity;
 end;
 
 opaque symbol rot_size_cat [a] (l1 l2:𝕃 a) :
@@ -1035,8 +1016,7 @@ end;
 
 opaque symbol rotr0 [a] (l:𝕃 a) : π (rotr 0 l = l) ≔
 begin
-  assume a l; simplify; rewrite take_size l; rewrite @drop_size a; //FIXME
-  reflexivity;
+  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) ≔
diff --git a/Nat.lp b/Nat.lp
index 3e72f58..78a6c41 100644
--- a/Nat.lp
+++ b/Nat.lp
@@ -772,7 +772,7 @@ opaque symbol ltn_trans x y z : π (istrue (x < y)) → π (istrue (y < z)) →
 begin
   assume x y z h i;
   have v:π (istrue (x +1 ≤ y +1)) { apply leqW (x +1) y h; };
-  apply @leq_trans (x +1) (y +1) z v i; //FIXME
+  apply @leq_trans (x +1) (y +1) z v i;
 end;
 
 opaque symbol <_asym x y : π (istrue (x < y)) → π (¬ (istrue (y < x))) ≔

From 3be03c47ecbfd6ab30c724fc1b27c22bb4ba81b1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Tue, 19 Nov 2024 13:46:32 +0100
Subject: [PATCH 2/2] wip

---
 CHANGES.md | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/CHANGES.md b/CHANGES.md
index 19d979b..0ddb7de 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -3,6 +3,10 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/),
 and this project adheres to [Semantic Versioning](https://semver.org/).
 
+## Unreleased
+
+- Declare istrue as injective
+
 ## 1.1.0 (2024-06-21)
 
 - Add classical logic