From f502843040ead28ef6a58764210f5e38a83d7206 Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Wed, 25 Jan 2023 15:45:36 +0100
Subject: [PATCH] Prepare for publication

Signed-off-by: Alban Gruin <alban.gruin@irit.fr>
---
 README                     |  36 ++++++++
 src/fivestage.v            |  52 ++++++------
 src/modular_definitions.v  |  15 ++--
 src/modular_store_buffer.v | 163 ++++++++++++++-----------------------
 src/utils.v                |  23 ++----
 5 files changed, 142 insertions(+), 147 deletions(-)
 create mode 100644 README

diff --git a/README b/README
new file mode 100644
index 0000000..d56f861
--- /dev/null
+++ b/README
@@ -0,0 +1,36 @@
+# Store buffer proofs in Coq
+This repository contains proofs related to store buffers in Coq.
+
+## Files
+In `src/` stand multiple files:
+
+ - `definitions.v`: defines multiple common types, functions and lemmas. Some
+   may be useless.
+ - `utils.v`: defines missing theorems and lemmas in the stdlib. Some may also
+   be useless.
+ - `storebuffer.v`: defines a parallel store buffer with granular locking, and
+   proves that it is monotonic. The proofs has multiple problems (it does not
+   take store buffer state changes into account, for instance), so this file
+   should be disregarded altogether. Also, lots of useless theorems. See this as
+   a playing ground for the next proofs.
+ - `correct_storebuffer.v`: defines a parallel store buffer with full locking,
+   and proves that it is monotonic.
+ - `granular_sb.v`: another parallel store buffer with granular locking, but
+   this time prove that it does not work when taking the state of the store
+   buffer into account.  This is done by finding a counter-example.
+
+## Dependencies
+This project was written with Coq 8.15.2, but it should work with Coq 8.14+. It
+will not work with older versions of Coq, because it uses some theorems that
+appeared in Coq 8.14.
+
+No external dependencies are used, and proofs are made in Ltac.
+
+## Building
+Assuming that you have Coq 8.14+ in your path. Execute the following commands in
+the root of the project:
+
+``` sh
+$ coq_makefile -f _CoqProject -o Makefile
+$ make
+```
diff --git a/src/fivestage.v b/src/fivestage.v
index e8eb6ad..ac24ecc 100644
--- a/src/fivestage.v
+++ b/src/fivestage.v
@@ -97,35 +97,35 @@ Definition nstg s :=
 Definition busFree := sbStateT_beq Empty.
 
 (* ready, free, and cycle functions. *)
-Definition ready next_id sbState (elt : instr_kind) :=
+Definition ready next_id sbState memNotFree (elt : instr_kind) :=
   match elt with
   | (_, (_, S _)) => false
   | (Store _ _, (Mem, 0)) => negb (sbStateT_beq Full sbState)
-  | (Load _ _, (Ex, 0)) => busFree sbState
+  | (Load _ _, (Ex, 0)) => busFree sbState && (negb memNotFree)
   | (opc, (Pre, 0)) => idx opc =? next_id
   | _ => true
   end.
 
-Definition memFree next_id sbState trace :=
+Definition memFree next_id sbState trace memNotFree :=
   let instr := get_instr_in_stage trace Mem in
   match instr with
-  | Some elt => ready next_id sbState elt
+  | Some elt => ready next_id sbState memNotFree elt
   | None => true
   end.
 
-Definition exFree next_id sbState trace :=
+Definition exFree next_id sbState trace memNotFree :=
   let instr := get_instr_in_stage trace Ex in
   match instr with
-  | Some elt => ready next_id sbState elt && memFree next_id sbState trace
+  | Some elt => ready next_id sbState memNotFree elt && memFree next_id sbState trace memNotFree
   | None => true
   end.
 
-Definition free next_id sbState trace (elt : instr_kind) :=
+Definition free next_id sbState trace memNotFree (elt : instr_kind) :=
   let (opc, state) := elt in
   let (st, _) := state in
   match nstg st with
-  | Mem => memFree next_id sbState trace
-  | Ex => exFree next_id sbState trace
+  | Mem => memFree next_id sbState trace memNotFree
+  | Ex => exFree next_id sbState trace memNotFree
   | _ => true
   end.
 
@@ -142,23 +142,26 @@ Definition get_latency opc st :=
   else
     0.
 
-Definition cycle_elt next_id sbState trace elt :=
+Definition cycle_elt next_id sbState trace memNotFree elt :=
   match elt with
   | (opc, (st, S n)) => (opc, (st, n))
   | (opc, (st, 0)) =>
-      if ready next_id sbState elt && free next_id sbState trace elt then
+      if ready next_id sbState memNotFree elt && free next_id sbState trace memNotFree elt then
         let nstg := nstg st in
         (opc, (nstg, get_latency opc nstg))
       else
         elt
   end.
 
+Definition memNotFree := List.existsb (is_in_stage Mem).
+
 Definition cycle sbState trace :=
-  List.map (cycle_elt (next_id trace) sbState trace) trace.
+  List.map (cycle_elt (next_id trace) sbState trace (memNotFree trace)) trace.
 
 Definition legal_sb_transitions st sbState sbState' :=
   match st, sbState with
   | Mem, NotEmpty => sbState' = NotEmpty \/ sbState' = Empty
+  | Ex, Empty => sbState' = Empty
   | Mem, Empty => sbState' = Empty
   | _, _ => sbState' = Full \/ sbState' = NotEmpty \/ sbState' = Empty
   end.
@@ -276,11 +279,10 @@ Section monotonicity.
       end.
 
   Hypothesis HfreePersists :
-    forall (st : stage), free (next_id t) sbState t (opc, (st, 0)) = true ->
-                    free (next_id t') sbState' t' (opc, (st, 0)) = true.
+    forall (st : stage), free (next_id t) sbState t (memNotFree t) (opc, (st, 0)) = true ->
+                    free (next_id t') sbState' t' (memNotFree t') (opc, (st, 0)) = true. (* TODO prove *)
 
-  Hypothesis HbusFree :
-    forall st, st = Ex -> busFree sbState = true -> busFree sbState' = true.
+  Hypothesis HmemUsed : st = Ex -> memNotFree t = false -> memNotFree t' = false. (* TODO prove *)
 
   Hypothesis HvalidLat : forall (e : instr_kind),
       match e with
@@ -305,8 +307,8 @@ Section monotonicity.
             rewrite Ht'
         end;
         unfold cycle;
-        rewrite (map_in_the_middle _ _ e d _ _ tpre tpost _ eq_refl Hi),
-          (map_in_the_middle _ _ _ d _ _ tpre' tpost' _ eq_refl Hi');
+        rewrite (map_in_the_middle _ _ e _ _ tpre tpost _ eq_refl Hi),
+          (map_in_the_middle _ _ _ _ _ tpre' tpost' _ eq_refl Hi');
         unfold cycle_elt;
         rewrite <- Ht;
         match type of He' with
@@ -325,11 +327,12 @@ Section monotonicity.
     Proof.
       intros He He' n.
       specialize (HfreePersists st).
-      specialize (HbusFree st).
+      (* specialize (HbusTaken e). *)
+      (* specialize (HbusFree st). *)
       specialize (HnIdLow t' e').
       specialize (HnIdHigh t' e').
 
-      rewrite Ht', <- He' in HnIdLow, HnIdHigh.
+      rewrite Ht', <- He' in HnIdLow, HnIdHigh, HmemUsed.
 
       (* Delve onto e, then handle stages on a case-by-case basis. *)
       work_on_e He'.
@@ -364,10 +367,9 @@ Section monotonicity.
             [| auto..].
 
           (* Loads *)
-          unfold ready.
-          destruct busFree.
-          * now rewrite HbusFree.
-          * discriminate.
+          destruct sbState; [| discriminate..].
+          destruct (memNotFree t); [discriminate |].
+          now rewrite Hlsbt, HmemUsed.
 
         + (* Case where e cannot progress in t. *)
           (* This is irrelevant, eliminate it. *)
@@ -495,7 +497,7 @@ Section monotonicity.
   End simple_monotonicity.
 
   Let tc_and_tc' :=
-        tc_tc'_length_eq (cycle_elt (next_id t) sbState t) (cycle_elt (next_id t') sbState' t')
+        tc_tc'_length_eq (cycle_elt (next_id t) sbState t (memNotFree t)) (cycle_elt (next_id t') sbState' t' (memNotFree t'))
           t t' tc tc' Hleb Htc Htc'.
 
   Variable e e' : instr_kind.
diff --git a/src/modular_definitions.v b/src/modular_definitions.v
index 8406180..373a608 100644
--- a/src/modular_definitions.v
+++ b/src/modular_definitions.v
@@ -8,6 +8,7 @@ Module Type Sig.
   Axiom first_stage : stage.
   Axiom stage_beq : stage -> stage -> bool.
   Axiom stage_beq_eq_true : forall s, stage_beq s s = true.
+  Axiom stage_beq_iff_eq : forall s s', stage_beq s s' = true <-> s = s'.
 
   Axiom leb : stage -> stage -> bool.
   Axiom idx : opcode -> nat.
@@ -37,6 +38,13 @@ Module Pipeline (Def : Sig).
           leb s1 s2
     end.
 
+  Fixpoint min_element l :=
+    match l with
+    | [] => 0
+    | x :: [] => x
+    | x :: l => Nat.min x (min_element l)
+    end.
+
   Definition next_id (trace : trace_kind) :=
     let filtered := List.filter (fun (elt : instr_kind) =>
                                    match elt with
@@ -46,10 +54,7 @@ Module Pipeline (Def : Sig).
                               match elt with
                               | (opc, _) => idx opc
                               end) filtered in
-    match mapped with
-    | [] => 0
-    | id :: r => List.fold_left Nat.min r id
-    end.
+    min_element mapped.
 
   Lemma state_leb_eq_true : forall st, state_leb st st = true.
   Proof.
@@ -84,7 +89,7 @@ Module Pipeline (Def : Sig).
 
   Definition pipeline_leb p1 p2 :=
     let comb := List.combine p1 p2 in
-    Nat.eqb (List.length p1) (List.length p2) && List.forallb instrs_leb comb.
+    (List.length p1 =? List.length p2) && List.forallb instrs_leb comb.
 
   Section comparison.
     Variable t t' : trace_kind.
diff --git a/src/modular_store_buffer.v b/src/modular_store_buffer.v
index 010959e..10da350 100644
--- a/src/modular_store_buffer.v
+++ b/src/modular_store_buffer.v
@@ -95,47 +95,36 @@ Definition nstg s opc :=
 Definition sbEmpty := sbStateT_beq Empty.
 
 (* ready, free and cycle functions. *)
-Definition ready next_id sbState (elt : instr_kind) :=
+Definition ready next_id sbState suNotFree (elt : instr_kind) :=
   match elt with
-  | (Load _ _, (Lsu, _)) => sbEmpty sbState
-  | (_, (Su, _)) => negb (sbStateT_beq sbState Full)
-  | (_, (Lu, S _)) => false
   | (opc, (Sp, 0)) => idx opc =? next_id
-  | _ => true
-  end.
-
-Definition luFree next_id sbState trace :=
-  let instr := get_instr_in_stage trace Lu in
-  match instr with
-  | Some elt => ready next_id sbState elt (* Sn is always free *)
-  | None => true
+  | (_, (Su, _)) => negb (sbStateT_beq sbState Full)
+  | (Load _ _, (Lsu, 0)) => sbEmpty sbState && (negb suNotFree)
+  | (_, (_, lat)) => lat =? 0
   end.
 
-Definition suFree next_id sbState trace :=
-  let instr := get_instr_in_stage trace Su in
+Definition luSuFree next_id sbState trace suNotFree stg :=
+  let instr := get_instr_in_stage trace stg in
   match instr with
-  | Some elt => ready next_id sbState elt (* Sn is always free *)
+  | Some elt => ready next_id sbState suNotFree elt (* Sn is always free *)
   | None => true
   end.
 
-Definition lsuFree next_id sbState trace :=
+Definition lsuFree next_id sbState trace suNotFree :=
   let instr := get_instr_in_stage trace Lsu in
   match instr with
-  | Some (opcode, (stg, lat)) => ready next_id sbState (opcode, (stg, lat)) &&
-                                  if stage_beq (nstg stg opcode) Lu then
-                                    luFree next_id sbState trace
-                                  else
-                                    suFree next_id sbState trace
+  | Some (opcode, (stg, lat)) => ready next_id sbState suNotFree (opcode, (stg, lat)) &&
+                                 luSuFree next_id sbState trace suNotFree (nstg stg opcode)
   | None => true
   end.
 
-Definition free next_id sbState trace (elt : instr_kind) :=
+Definition free next_id sbState trace suNotFree (elt : instr_kind) :=
   let (opc, state) := elt in
   let (st, _) := state in
   match nstg st opc with
-  | Lu => luFree next_id sbState trace
-  | Su => suFree next_id sbState trace
-  | Lsu => lsuFree next_id sbState trace
+  | Lu => luSuFree next_id sbState trace suNotFree Lu
+  | Su => luSuFree next_id sbState trace suNotFree Su
+  | Lsu => lsuFree next_id sbState trace suNotFree
   | _ => true
   end.
 
@@ -152,7 +141,7 @@ Definition get_latency opc st :=
   else
     0.
 
-Definition cycle_elt next_id (busTaken : bool) sbState trace elt :=
+Definition cycle_elt next_id busTaken sbState trace suNotFree elt :=
   match elt with
   | (opc, (st, S n)) =>
       if (negb (stage_beq Lu st)) || busTaken then
@@ -160,18 +149,22 @@ Definition cycle_elt next_id (busTaken : bool) sbState trace elt :=
       else
         elt
   | (opc, (st, 0)) =>
-      if ready next_id sbState elt && free next_id sbState trace elt then
+      if ready next_id sbState suNotFree elt && free next_id sbState trace suNotFree elt then
         let nstg := nstg st opc in
         (opc, (nstg, get_latency opc nstg))
       else
         elt
   end.
 
+Definition suNotFree := List.existsb (is_in_stage Su).
+Definition luNotFree := List.existsb (is_in_stage Lu).
+
 Definition cycle sbState busTaken trace :=
-  List.map (cycle_elt (next_id trace) busTaken sbState trace) trace.
+  List.map (cycle_elt (next_id trace) busTaken sbState trace (suNotFree trace)) trace.
 
 Definition legal_sb_transitions st sbState sbState' :=
   match st, sbState with
+  | Lsu, Empty => sbState' = Empty
   | Su, Empty => sbState' = Empty
   | Su, NotEmpty => sbState' = NotEmpty \/ sbState' = Empty
   | _, _ => sbState' = Full \/ sbState' = NotEmpty \/ sbState' = Empty
@@ -316,17 +309,16 @@ Section monotonicity.
 
   (* Long hypotheses related to stage occupation. *)
   Hypothesis HfreeLsuPersists :
-    free (next_id t) sbState t (opc, (Sp, 0)) = true ->
-    free (next_id t') sbState' t' (opc, (Sp, 0)) = true.
+    free (next_id t) sbState t (suNotFree t) (opc, (Sp, 0)) = true ->
+    free (next_id t') sbState' t' (suNotFree t') (opc, (Sp, 0)) = true. (* TODO prove *)
 
   Hypothesis HfreeFromLsuPersists :
-    free (next_id t) sbState t (opc, (Lsu, 0)) = true ->
-    free (next_id t') sbState' t' (opc, (Lsu, 0)) = true.
-
-  Hypothesis HbusTakenPersists : busTaken = true -> busTaken' = true.
+    free (next_id t) sbState t (suNotFree t) (opc, (Lsu, 0)) = true ->
+    free (next_id t') sbState' t' (suNotFree t') (opc, (Lsu, 0)) = true. (* TODO prove *)
 
-  Hypothesis HsbRemainsEmpty :
-    forall st, st = Lsu -> sbEmpty sbState = true -> sbEmpty sbState' = true.
+  Hypothesis HsuUsed : st = Lsu -> suNotFree t = false -> suNotFree t' = false. (* TODO prove *)
+  Hypothesis HluUsed : st = Lsu -> luNotFree t = false -> luNotFree t' = false. (* TODO prove *)
+  Hypothesis HbusTaken : forall st n busTaken, st = Lu -> n <> 0 -> busTaken = true.
 
   Hypothesis HvalidLat : forall (e : instr_kind),
   match e with
@@ -351,8 +343,8 @@ Section monotonicity.
             rewrite Ht'
         end;
         unfold cycle;
-        rewrite (map_in_the_middle _ _ e d _ _ tpre tpost _ eq_refl Hi),
-          (map_in_the_middle _ _ _ d _ _ tpre' tpost' _ eq_refl Hi');
+        rewrite (map_in_the_middle _ _ e _ _ tpre tpost _ eq_refl Hi),
+          (map_in_the_middle _ _ _ _ _ tpre' tpost' _ eq_refl Hi');
         unfold cycle_elt;
         rewrite <- Ht;
         match type of He' with
@@ -372,16 +364,6 @@ Section monotonicity.
              auto)
         ].
 
-    Ltac busTaken_delve :=
-      destruct (negb _);
-        simpl (if (_ || _) then _ else _);
-        [|
-          destruct busTaken; [
-            rewrite (HbusTakenPersists eq_refl) |
-            destruct busTaken'
-          ]
-        ].
-
     Lemma unmoved_no_lat_can_advance :
       e = (opc, (st, 0)) -> e = e' -> forall n,
       List.nth_error tc i = Some (opc, (nstg st opc, n)) ->
@@ -390,11 +372,10 @@ Section monotonicity.
       intros He He' n.
       specialize (Hlu st opc).
       specialize (Hsu st opc).
-      specialize (HsbRemainsEmpty st).
       specialize (HnIdLow t' e').
       specialize (HnIdHigh t' e').
 
-      rewrite Ht', <- He' in HnIdLow, HnIdHigh.
+      rewrite Ht', <- He' in HnIdLow, HnIdHigh, HsuUsed, HluUsed.
 
       (* Delve onto e, then handle stages on a case-by-case basis. *)
       work_on_e He'.
@@ -407,12 +388,11 @@ Section monotonicity.
           unfold ready.
           repeat rewrite opc_match_case_identical.
 
-          destruct (_ =? _) eqn:Hidx.
-          * rewrite Nat.eqb_eq in Hidx.
-            rewrite <- Hidx in HnId.
-            destruct HnIdHigh as [_ HnIdHigh'].
-            now rewrite <- (n_le_he_eq _ _ HnId (HnIdHigh' eq_refl)), Nat.eqb_refl.
-          * discriminate.
+          destruct (_ =? _) eqn:Hidx; [| discriminate].
+          rewrite Nat.eqb_eq in Hidx.
+          rewrite <- Hidx in HnId.
+          destruct HnIdHigh as [_ HnIdHigh'].
+          now rewrite <- (n_le_he_eq _ _ HnId (HnIdHigh' eq_refl)), Nat.eqb_refl.
 
         + (* LSU is not free in t: this is irrelevant. *)
           rewrite andb_false_r.
@@ -422,14 +402,15 @@ Section monotonicity.
       - destruct free, opc.
         (* Cases where e progressed in t. *)
         + (* Loads *)
-          unfold ready.
-          destruct sbEmpty.
-          * simpl in HfreeFromLsuPersists |- *.
-            now rewrite HsbRemainsEmpty, HfreeFromLsuPersists.
-          * discriminate.
+          simpl in Hlsbt, HfreeFromLsuPersists |- *.
+          destruct sbState; [| discriminate..].
+          subst sbState'.
+          rewrite (HfreeFromLsuPersists eq_refl).
+          destruct (suNotFree t); [discriminate |].
+          now rewrite HsuUsed.
+
         + (* Stores *)
-          simpl in HfreeFromLsuPersists |- *.
-          now rewrite HfreeFromLsuPersists.
+          now rewrite <- HfreeFromLsuPersists.
 
         (* Cases where e did not progress in t. *)
         (* Irrelevant, exclude them. *)
@@ -443,8 +424,11 @@ Section monotonicity.
       (* Su: if there is space in the store buffer, move to Sn, otherwise, remain
        in Su.  Eliminate cases where sbState/sbState' are inconsistent. *)
       - stage_opc Hsu.
-        now destruct sbState, sbState', Hlsbt;
-          try discriminate.
+        simpl in Hlsbt.
+        destruct sbState; [..| discriminate].
+        + now rewrite Hlsbt.
+        + destruct Hlsbt as [HsbState' | HsbState'];
+            now rewrite HsbState'.
 
       (* Sn: instructions remains in Sn. *)
       - auto.
@@ -455,6 +439,7 @@ Section monotonicity.
                 compare_two (List.nth_error tc i) (List.nth_error tc' i) = true.
     Proof.
       intros n He He'.
+      specialize (HbusTaken st n).
 
       (* Extract e. *)
       pose proof unmoved_no_lat_can_advance as Huca.
@@ -478,26 +463,11 @@ Section monotonicity.
              * is also trivial. *)
             now apply compare_two_eq_true.
 
-      - (* Case where an instruction has a latency higher than 0. *)
-        (* We have e = e' = (opc, (st, S n)) *)
-        busTaken_delve.
-        + (* Case where st <> Lu: both can progress. *)
-          (* cycle_elt ... e = cycle_elt ... e': compare_two ... = true. *)
-          now apply compare_two_eq_true.
-
-        (* Cases where st = Lu. *)
-        + (* busTaken = true -> busTaken' = true, both can progress. *)
-          (* cycle_elt ... e = cycle_elt ... e': compare_two ... = true. *)
-          now apply compare_two_eq_true.
-        + (* busTaken = false, busTaken' = true. *)
-          (* cycle_elt ... e = e, cycle_elt ... e' = (opc, (st, n)). *)
-          (* compare_two ... = n <=? S n.  This is trivial. *)
-          simpl.
-          rewrite stage_beq_eq_true, Nat.leb_le.
+      - destruct st;
+          try (simpl;
+                 now rewrite Nat.leb_refl).
+        rewrite (HbusTaken busTaken), (HbusTaken busTaken');
           auto.
-        + (* busTaken = false, busTaken' = false, both can't progress. *)
-          (* cycle_elt ... e = cycle_elt ... e': compare_two ... = true. *)
-          now apply compare_two_eq_true.
     Qed.
 
     Lemma moved_lat_left_is_monotonic :
@@ -635,25 +605,12 @@ Section monotonicity.
       - (* n and n' <> 0. *)
         destruct (stage_eq_dec st st') as [Heq | Hdiff].
         + (* st = st'. *)
-          (* In the worst case, we have:
-           * compare_two (opc, (st, n - 1)) (opc, (st, n')) = true
-           * We know that n > n' (cf. assumptions), so n - 1 >= n'.
-           * The proposition is true.
-           * Other cases are:
-           * compare_two (opc, (st, n)) (opc, (st, n')) = true
-           * compare_two (opc, (st, n - 1)) (opc, (st, n' - 1)) = true
-           * Both propositions are true. *)
           rewrite Heq in Hsl |- *.
-          busTaken_delve;
-            (* Take care of cases where both instructions can or cannot
-             * progress automatically. *)
+          specialize (HbusTaken st').
+          destruct st';
+            try auto.
+          rewrite (HbusTaken (S n) busTaken), (HbusTaken (S n') busTaken');
             auto.
-          * (* st = Lu.  busTaken = false, busTaken' = true. *)
-            (* e = (opc, (st', S n)), e' = (opc, (st', S n')). *)
-            (* S n' <=? S n.  We must prove that n' <=? S n. *)
-            simpl.
-            rewrite stage_beq_eq_true, Nat.leb_le in Hsl |- *.
-            lia.
 
         + (* st <> st'. *)
           (* Both instructions will remain in their respective stages.
@@ -687,8 +644,8 @@ Section monotonicity.
   End simple_monotonicity.
 
   Let tc_and_tc' :=
-        tc_tc'_length_eq (cycle_elt (next_id t) busTaken sbState t)
-          (cycle_elt (next_id t') busTaken' sbState' t')
+        tc_tc'_length_eq (cycle_elt (next_id t) busTaken sbState t (suNotFree t))
+          (cycle_elt (next_id t') busTaken' sbState' t' (suNotFree t'))
           t t' tc tc' Hleb Htc Htc'.
 
   Variable e e' : instr_kind.
diff --git a/src/utils.v b/src/utils.v
index 19c7b2c..395d8d4 100644
--- a/src/utils.v
+++ b/src/utils.v
@@ -1,21 +1,20 @@
 Require Import Lia List Nat.
 Import ListNotations.
 
-Lemma list_elt_exists :
-  forall (A : Type) (l : list A) (d : A) i,
+Lemma list_elt_exists : forall (A : Type) (l : list A) i,
     i < List.length l -> (exists a, List.nth_error l i = Some a).
 Proof.
-  intros A l d i Hi.
+  intros A l i Hi.
   destruct nth_error eqn:Hnth.
   - now exists a.
-  - pose proof (nth_error_nth' l d Hi) as Hnth'.
-    rewrite Hnth in Hnth'.
-    discriminate.
+  - destruct (nth_error_None l i) as [HNone _].
+    specialize (HNone Hnth).
+    lia.
 Qed.
 
 Section list_utils.
   Variable A B : Type.
-  Variable a d : A.
+  Variable a : A.
   Variable f : A -> B.
   Variable l lpre lpost : list A.
   Variable i : nat.
@@ -30,14 +29,10 @@ Section list_utils.
     lia.
   Qed.
 
-  Lemma nth_error_on_composed_list : List.nth_error l i = Some a.
-  Proof.
-    now rewrite (nth_error_nth' _ d i_lt_length_l), Hl, Hi, nth_middle.
-  Qed.
-
   Lemma map_in_the_middle : List.nth_error (List.map f l) i = Some (f a).
   Proof.
-    apply map_nth_error, nth_error_on_composed_list.
+    apply List.map_nth_error.
+    now rewrite Hl, Hi, List.nth_error_app2, PeanoNat.Nat.sub_diag.
   Qed.
 
   Lemma list_is_composed :
@@ -49,7 +44,7 @@ Section list_utils.
     pose proof i_lt_length_l as Hlength'.
     rewrite Hlength in Hlength'.
 
-    pose proof (list_elt_exists A l' d i Hlength') as Hle.
+    pose proof (list_elt_exists _ _ _ Hlength') as Hle.
     destruct Hle as [a' Hle].
 
     pose proof (nth_error_split l' i Hle) as Hnes.
-- 
GitLab