Update environment

src/Environment.v

-From Coq Require Import Arith ZArith Psatz Bool Ascii String List FunInd Program Program.Equality Program.Wf BinNums BinaryString.
-
-From mathcomp Require Import ssreflect ssrbool seq.
-
+From Coq Require Import Arith ZArith Psatz Bool
+                        Ascii String List FunInd Program
+                        Program.Equality Program.Wf BinNums BinaryString.
 
 From VFP Require Import BasicTypes
                         FPNavigationMode
@@ -9,7 +8,10 @@ From VFP Require Import BasicTypes
                         CLightGen
                         FPExtended.
 
-Local Open Scope list_scope.
+Set Warnings "-parsing".
+From mathcomp Require Import ssreflect seq.
+Set Warnings "parsing".
+
 Local Open Scope string_scope.
 Import ListNotations.
 Require Import FunInd.
@@ -687,7 +689,8 @@ Module ENVS (EVAL_Def: EVAL_ENV).
       inversion Hnth.
 
       apply equiv_while with (nb := nb) (n' := ids'0)
-                              (n'' := n') (p_e' := p'0); try lia.
+                              (n'' := n') (p_e' := p'0);
+                              rewrite -?plusE -?minusE; try lia.
       * apply IHequiv_stages1; by apply equiv_fpe_stages_take.
       * by rewrite -H16.
       * apply IHequiv_stages2. by apply equiv_fpe_stages_drop.

src/FPExtended.v

@@ -4,7 +4,7 @@ From compcert Require Import Coqlib Integers Floats AST Ctypes
                              Cop Clight Clightdefs.
 
 Set Warnings "-parsing".
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import ssreflect ssrnat. (* TODO add seq*)
 Set Warnings "parsing".
 Import ListNotations.
 
@@ -537,15 +537,15 @@ Admitted.
 (** TODO: Common lemmas about list, maybe to move outside *)
 Lemma cons_last:
   forall A (e e' d : A) l,
-    last d (e :: e' :: l) = last d (e' :: l).
+    last (e :: e' :: l) d = last (e' :: l) d.
 Proof.
   by [].
 Qed.
 
 Lemma map_last:
   forall A B (f: A -> B) d0 l0 e,
-    e = last d0 l0
-    -> f e = last (f d0) (map f l0).
+    e = last l0 d0
+    -> f e = last (map f l0) (f d0).
 Proof.
   move => A B f d0 [|e' l0] e.
   - move => He; by rewrite He.
@@ -559,9 +559,9 @@ Qed.
 Lemma map_last_split:
   forall A B (f: A -> B) d0 d1 l0 l1 e,
     d1 = f d0
-    -> e = last d0 l0
+    -> e = last l0 d0
     -> l1 = map f l0
-    -> f e = last d1 l1.
+    -> f e = last l1 d1.
 Proof.
   move => A B f d0 d1 l0 l1 e Hd He Hl.
   rewrite Hl Hd. by apply map_last.
@@ -589,9 +589,10 @@ Proof.
           /extend_flight_plan
   => fp [[fb e [b bs]] Hwf] Hfp //=; injection Hfp as Hfb He Hex Hm.
   assert (H: extend_block
-      (last (FP.get_blocks_hd (FP.get_fp_blocks fp))
-            (FP.get_blocks_tl (FP.get_fp_blocks fp)))
-        = last b bs).
+      (last (FP.get_blocks_tl (FP.get_fp_blocks fp))
+            (FP.get_blocks_hd (FP.get_fp_blocks fp))
+            )
+        = last bs b).
   { apply map_last_split with
                   (d0 := FP.get_blocks_hd (FP.get_fp_blocks fp))
                   (l0 := FP.get_blocks_tl (FP.get_fp_blocks fp));