same run_step Incorrect and normalize if ids = 0

src/semantics/FPBigStepSized.v

@@ -1317,6 +1317,60 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
       + apply correct_through_app_trace.
         apply (correct_through_run_step). apply Hc2.
   Qed.
+
+  Lemma Incorrect_idb_getstage_default : forall e,
+    ~semi_correct_env e -> 
+    FP_E.get_stages (` (` fps)) (get_nav_block e) = get_block_stages (get_default_block (` (` fps))).
+  Proof.
+    intros e Nsc. unfold get_stages.
+    unfold semi_correct_env in Nsc. simpl in Nsc. unfold correct_block_id in Nsc.
+    assert (FP_E.get_block (FPE_BS.fp (` fps)) (get_nav_block e) = (get_default_block (FPE_BS.fp (` fps)) )).
+    apply get_block_default_block. unfold FPE_BS.fp. ssrlia.
+    unfold FPE_BS.fp in H. rewrite H. reflexivity.
+  Qed.
+
+  Lemma Incorrect_idb_same_run_step_normalize_0 : forall e e1 e2,
+    ~semi_correct_env e -> get_nav_stage e = 0 ->
+    run_step (` fps) e = e1 -> run_step (` fps) (normalise (` (` fps)) e) = e2 -> 
+    e2 = (normalise (` (` fps)) e1).
+  Proof.
+    intros e.
+    rewrite run_step_equation. rewrite (run_step_equation (` fps) (normalise (` (` fps)) e)).
+    destruct (run_stage (` fps) e) as [b1 e1] eqn:Estage1.
+    destruct (run_stage (` fps) (normalise (` (` fps)) e)) as [b2 e2] eqn:Estage2.
+    remember (normalise (` (` fps)) e) as e'. unfold normalise in Heqe'.
+    unfold FP_E.normalise_block_id in Heqe'.
+    intros e0 e3 Hidb. unfold semi_correct_env in Hidb.
+    unfold correct_block_id in Hidb.
+    assert (get_nb_block (` (` fps)) <=? get_nav_block e = true).
+    { destruct (get_nb_block (` (` fps)) <=? get_nav_block e) eqn:E. reflexivity.
+      exfalso. apply Hidb. apply leb_complete_conv in E. apply E. }
+    rewrite H in Heqe'. rename H into Hidb2.
+    generalize dependent e3. generalize dependent e0.
+    - unfold run_stage in Estage1, Estage2.
+      unfold FPE_BS.fp in Estage1, Estage2.
+      remember (get_current_stage (` (` fps)) e ) as stage1.
+      remember (get_current_stage (` (` fps)) e') as stage2.
+      unfold get_current_stage in Heqstage1, Heqstage2.
+      unfold get_stage in Heqstage1, Heqstage2.
+      rewrite (Incorrect_idb_getstage_default Hidb) in Heqstage1.
+      unfold get_stages in Heqstage2.
+      assert (Hgp2 : FP_E.get_block (` (` fps)) (get_nav_block e') = get_default_block (` (` fps))).
+      apply get_block_default_block. rewrite Heqe'. unfold mk_fp_env. simpl.
+      ssrlia.
+      rewrite Hgp2 in Heqstage2.
+      assert (get_nav_stage e = get_nav_stage e').
+      rewrite Heqe'. reflexivity.
+      rewrite H in Heqstage1. simpl in Heqstage1, Heqstage2.
+      intros e1' e2' Hstage He1 He2. rewrite H in Hstage. simpl in Hstage.
+      rewrite Hstage in Heqstage1, Heqstage2. subst. clear H. clear Hstage.
+      inversion Estage1; inversion Estage2; subst; clear Estage2; clear Estage1.
+
+      destruct e as [st t]. unfold mk_fp_env. unfold app_trace. simpl.
+      unfold normalise. unfold mk_fp_env. simpl.
+      unfold FP_E.normalise_block_id. simpl in Hidb. rewrite Hidb2.
+      reflexivity.
+  Qed.
   End FLIGHT_PLAN.
 
   Definition step_size (fps: flight_plan_sized) (e e': fp_env8) :=

[WASQUEL Valentin]

calling a run_step for an environment with an incorrect block id will have a same result as doing it with the normalised block id (fixing the block id) if the current stage is 0 : when a env have an incorrect block id, it is the same as having the default block. default block have one nav HOME stage and then the default stage.

any stage id other than 0 will change the block id to the default block. it is not the same result as doing it with the id of the block already normalize (which put it as the default id) because when changing block to a block of the same id, lidb and lids will not be changed so we have a different result.