UNFINISHED ! proof step e or normalise same trace

src/semantics/FPBigStepSized.v

@@ -1112,6 +1112,17 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
       destruct (get_nav_block e =? new_id)%N; 
       apply normalise_block_id_is_correct.
     Qed.
+
+    Lemma semi_correct_change_block_is_correct : forall e new_id,
+      semi_correct_env e -> get_nav_block e <> new_id ->
+      correct_env (change_block (` (` fps)) e new_id).
+    Proof.
+      intros e new_id Hsc Hid. unfold change_block.
+      apply Nat.eqb_neq in Hid. rewrite Hid. simpl.
+      split.
+      - apply normalise_block_id_is_correct.
+      - apply Hsc.      
+    Qed.
     
     Lemma correct_through_change_block : forall e new_id,
       correct_env e -> correct_env (change_block (` (` fps)) e new_id).
@@ -1497,6 +1508,323 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
       apply Nsc'. rewrite <- Eids. apply Hids.
   Qed.
 
+  Lemma normalise_get_from : forall id1 fb,
+    id1 =? get_fbd_from fb = (normalise_block_id (` (` fps)) id1 =? get_fbd_from fb).
+  Proof.
+    intros id1 fb.
+    unfold normalise_block_id. destruct (get_nb_block (` (` fps)) <=? id1) eqn:E.
+    - have H := (All_forbidden_derout_from_user_block fb).
+      apply leb_complete in E. to_nat H.
+      assert (id1 =? get_fbd_from fb = false) by (apply Nat.eqb_neq; ssrlia).
+      rewrite H0.
+      assert ((get_nb_block (` (` fps)) - 1)%coq_nat =? get_fbd_from fb = false) by (apply Nat.eqb_neq; ssrlia).
+      rewrite H1. reflexivity.
+    - reflexivity.
+  Qed.
+
+  Lemma normalise_get_exception_block_id : forall id1 fb,
+    get_expt_block_id fb =? id1 = (get_expt_block_id fb =? normalise_block_id (` (` fps)) id1).
+  Proof.
+    intros id1 fb.
+    unfold normalise_block_id. destruct (get_nb_block (` (` fps)) <=? id1) eqn:E.
+    - have H := (All_exception_to_user_block fb).
+      apply leb_complete in E. to_nat H.
+      transitivity false.
+      apply Nat.eqb_neq; ssrlia.
+      symmetry.
+      apply Nat.eqb_neq; ssrlia.
+    - reflexivity.
+  Qed.
+
+  Lemma Incorrect_idb_test_forbidden_deroute_same_trace_normalise: forall e id1 id2 fb e1 b1 e2 b2,
+    ~semi_correct_env e -> 
+    Common_Sem.test_forbidden_deroute e id1 id2 fb = (b1, e1) -> 
+    Common_Sem.test_forbidden_deroute (normalise (` (` fps)) e) (normalise_block_id (` (` fps)) id1) id2 fb = (b2, e2) ->
+      get_trace e1 = get_trace e2 /\ b1 = b2.
+  Proof.
+    unfold Common_Sem.test_forbidden_deroute. intros e id1 id2 fb e1 b1 e2 b2 Nsc.
+    rewrite <- (normalise_get_from id1 fb).
+    destruct ((id1 =? get_fbd_from fb) && (id2 =? get_fbd_to fb)).
+    - destruct (get_fbd_only_when fb).
+      + unfold evalc. intros H1 H2. inversion H1; inversion H2. split; reflexivity.
+      + intros H1 H2. inversion H1; inversion H2. subst. split; auto.
+    - intros H1 H2. inversion H1; inversion H2. subst. split; auto.
+  Qed.
+
+  Lemma normalise_through_test_forbidden_deroute : forall e id1 id2 b e' fb,
+    Common_Sem.test_forbidden_deroute e id1 id2 fb = (b, e') ->
+    Common_Sem.test_forbidden_deroute (normalise (` (` fps)) e) (normalise_block_id (` (` fps)) id1) id2 fb = (b, (normalise (` (` fps)) e')).
+  Proof.
+    intros e id1 id2 b e' fb. unfold Common_Sem.test_forbidden_deroute.
+    rewrite <- (normalise_get_from id1 fb).
+    destruct ((id1 =? get_fbd_from fb) && (id2 =? get_fbd_to fb)).
+    - destruct (get_fbd_only_when fb).
+      + unfold evalc. intro H. inversion H. simpl.
+        unfold normalise. unfold app_trace. reflexivity.
+      + intros H. inversion H. reflexivity.
+    - intros H. inversion H. reflexivity.
+  Qed.
+
+  Lemma Incorrect_idb_test_forbidden_deroutes_same_trace_normalise: forall e id2 lfb e1 b1 e2 b2,
+    ~semi_correct_env e -> 
+    Common_Sem.test_forbidden_deroutes e (get_nav_block e) id2 lfb = (b1, e1) -> 
+    Common_Sem.test_forbidden_deroutes (normalise (` (` fps)) e) (normalise_block_id (` (` fps)) (get_nav_block e)) id2 lfb = (b2, e2) ->
+      get_trace e1 = get_trace e2 /\ b1 = b2.
+  Proof.
+    intros e id2 lfb. generalize dependent e. induction lfb.
+    - simpl. intros e e1 b1 e2 b2 Nsc H1 H2.
+      inversion H1; inversion H2; subst; split; auto.
+
+    - simpl. intros e e1 b1 e2 b2 Nsc.
+      destruct (Common_Sem.test_forbidden_deroute e _ id2 a) as [b e'] eqn:Test1.
+      destruct (Common_Sem.test_forbidden_deroute (normalise (` (` fps)) e) (normalise_block_id (` (` fps)) _ ) id2 a) as [b' e''] eqn:Test2.
+      destruct (Incorrect_idb_test_forbidden_deroute_same_trace_normalise _ _ _ Nsc Test1 Test2).
+      subst.
+      destruct b'.
+      + intros H1 H2. inversion H1; inversion H2; subst. split; auto.
+      + have H1 := (normalise_through_test_forbidden_deroute _ _ _ _ Test1).
+        rewrite Test2 in H1. inversion H1. clear H1. subst.
+        have H1 := (test_forbidden_deroute_nraised_unchanged _ _ _ Test1).
+        simpl in H1. rewrite H1.
+        simpl in IHlfb. apply IHlfb.
+        unfold semi_correct_env. simpl. rewrite <- H1.
+        apply Nsc.
+  Qed.
+
+  Lemma normalise_through_test_forbidden_deroutes : forall e id2 lfb e1 b1,
+    Common_Sem.test_forbidden_deroutes e (get_nav_block e) id2 lfb = (b1, e1) -> 
+    Common_Sem.test_forbidden_deroutes (normalise (` (` fps)) e) (normalise_block_id (` (` fps)) (get_nav_block e)) id2 lfb
+     = (b1, (normalise (` (` fps)) e1)).
+  Proof.
+    intros e id2 lfb. generalize dependent e. induction lfb.
+    - simpl. intros e e1 b1 H1. inversion H1. reflexivity.
+    - simpl. intros e e1 b1.
+      destruct (Common_Sem.test_forbidden_deroute e (nav_block (get_state e)) id2 a)
+      as [b e'] eqn:Testfb.
+
+      have Testfb2 := (normalise_through_test_forbidden_deroute _ _ _ _ Testfb).
+      rewrite Testfb2.
+      destruct b. 
+      + intros H. inversion H. reflexivity.
+      + 
+        have H1 := (test_forbidden_deroute_nraised_unchanged _ _ _ Testfb).
+        simpl in H1. rewrite H1.
+        apply IHlfb.
+  Qed.
+
+  Lemma Incorrect_idb_forbidden_deroutes_same_trace_normalise: forall e new_id e1 b1 e2 b2,
+    ~semi_correct_env e -> 
+    Common_Sem.forbidden_deroute (` (` fps)) e new_id = (b1, e1) -> 
+    Common_Sem.forbidden_deroute (` (` fps)) (normalise (` (` fps)) e) new_id = (b2, e2) ->
+      get_trace e1 = get_trace e2 /\ b1 = b2.
+  Proof.
+    unfold Common_Sem.forbidden_deroute. intros e new_id e1 b1 e2 b2. 
+    apply Incorrect_idb_test_forbidden_deroutes_same_trace_normalise.
+  Qed.
+
+  Lemma normalise_through_forbidden_deroute : forall e new_id e1 b1,
+    Common_Sem.forbidden_deroute (` (` fps)) e new_id = (b1, e1) -> 
+    Common_Sem.forbidden_deroute (` (` fps)) (normalise (` (` fps)) e) new_id
+     = (b1, (normalise (` (` fps)) e1)).
+  Proof.
+    unfold Common_Sem.forbidden_deroute. intros e new_id e1 b1. 
+    apply normalise_through_test_forbidden_deroutes.
+  Qed.
+  
+  Lemma Incorrect_idb_goto_same_trace_normalise: forall e new_id e1 e2,
+    ~semi_correct_env e -> 
+    Common_Sem.goto_block (` (` fps)) e new_id = e1 -> 
+    Common_Sem.goto_block (` (` fps)) (normalise (` (` fps)) e) new_id = e2 ->
+      get_trace e1 = get_trace e2.
+  Proof.
+    unfold Common_Sem.goto_block. intros e new_id e1 e2 Nsc.
+    destruct (Common_Sem.forbidden_deroute (` (` fps)) e new_id) as [res1 e1'] eqn:fb1.
+    destruct (Common_Sem.forbidden_deroute (` (` fps)) (normalise (` (` fps)) e) new_id) as [res2 e2'] eqn:fb2.
+    destruct (Incorrect_idb_forbidden_deroutes_same_trace_normalise _ Nsc fb1 fb2).
+    subst. destruct res2.
+    - intros. subst. auto.
+    - unfold Common_Sem.c_change_block.
+      unfold Common.on_exit.
+      assert (FP_E.get_block (` (` fps)) (get_nav_block e) = get_default_block (` (` fps))).
+        apply get_block_default_block.
+        unfold semi_correct_env in Nsc. unfold correct_block_id in Nsc. unfold FPE_BS.fp. to_nat Nsc. ssrlia.
+        rewrite H0. 
+      assert (FP_E.get_block (` (` fps)) (get_nav_block (normalise (` (` fps)) e)) = get_default_block (` (` fps))).
+        apply get_block_default_block.
+        unfold normalise. simpl. unfold normalise_block_id.
+        unfold semi_correct_env in Nsc. unfold correct_block_id in Nsc. unfold FPE_BS.fp. to_nat Nsc.
+        destruct (FP_E.get_nb_block (` (` fps)) <=? nav_block (get_state e));
+        ssrlia.
+      rewrite H1.
+      clear H0; clear H1.
+      unfold change_block.
+      destruct (get_nav_block e1' =? new_id);
+      destruct (get_nav_block e2' =? new_id);
+      unfold app_trace; simpl; intros H1; intros H2; subst; simpl; rewrite H; reflexivity.
+  Qed.
+  
+  Lemma Incorrect_idb_test_exception_same_trace_normalise: forall e ex e1 b1 e2 b2,
+    ~semi_correct_env e -> 
+    Common_Sem.test_exception (` (` fps)) e ex = (b1, e1) -> 
+    Common_Sem.test_exception (` (` fps)) (normalise (` (` fps)) e) ex = (b2, e2) ->
+      get_trace e1 = get_trace e2 /\ b1 = b2.
+  Proof.
+    intros e ex e1 b1 e2 b2 Nsc. unfold semi_correct_env in Nsc.
+    unfold correct_block_id in Nsc. to_nat Nsc.
+    unfold Common_Sem.test_exception.
+    rewrite  (normalise_get_exception_block_id (get_nav_block e) ex).
+    simpl.
+    assert (get_expt_block_id ex =? normalise_block_id (` (` fps)) (nav_block (get_state e)) = false).
+      have H := (All_exception_to_user_block ex).
+      to_nat H. apply Nat.eqb_neq. unfold normalise_block_id.
+      destruct (get_nb_block (` (` fps)) <=? nav_block (get_state e)); ssrlia.
+    rewrite H. clear H.
+    unfold normalise. simpl.
+    destruct (~~ EVAL_Def.eval (get_trace e) (get_expt_cond ex)).
+    - unfold app_trace. simpl.
+      intros H1 H2. inversion H1; inversion H2. split; reflexivity.
+      
+    - unfold app_trace. simpl. 
+      intros H1 H2. inversion H1; inversion H2. clear H0. clear H4.
+      rewrite H3. rewrite H5. split.
+      + eapply Incorrect_idb_goto_same_trace_normalise with (e := {|
+        get_state := get_state e;
+        get_trace_env :=
+          (get_trace e ++
+           [:: COND (get_expt_cond ex)
+                 (EVAL_Def.eval (get_trace e) (get_expt_cond ex))]) ++
+          opt_c_code_to_trace (get_expt_exec ex)
+        |}).
+        apply Nsc.
+        apply H3. apply H5.
+      + reflexivity.
+  Qed.
+
+  Lemma normalise_through_test_exception_false : forall e a e',
+    Common_Sem.test_exception (` (` fps)) e a = (false, e') ->
+    Common_Sem.test_exception (` (` fps)) (normalise (` (` fps)) e) a = (false, (normalise (` (` fps)) e')).
+  Proof.
+    unfold Common_Sem.test_exception. unfold normalise. simpl. intros e a.
+    rewrite  (normalise_get_exception_block_id (get_nav_block e) a). simpl.
+    destruct (get_expt_block_id a =? normalise_block_id (` (` fps)) (nav_block (get_state e))).
+    - intros e' H. inversion H. reflexivity.
+    - destruct (~~ EVAL_Def.eval (get_trace e) (get_expt_cond a)).
+      + intros e' H. inversion H.
+        reflexivity.
+      + intros e' H. inversion H.
+  Qed.
+
+  Lemma Incorrect_idb_through_test_exception_false : forall e a e',
+    ~semi_correct_env e ->
+    Common_Sem.test_exception (` (` fps)) e a = (false, e') ->
+    ~semi_correct_env e'.
+  Proof.
+    intros e a e' Nsc.
+    unfold Common_Sem.test_exception.
+    destruct (get_expt_block_id a =? get_nav_block e).
+    - intros H. inversion H. subst. auto.
+
+    - unfold evalc. destruct (~~ EVAL_Def.eval (get_trace e) (get_expt_cond a));
+      intros H; inversion H.
+      apply Nsc.
+  Qed.
+  
+  Lemma Incorrect_idb_test_exceptions_same_trace_normalise: forall e lex e1 b1 e2 b2,
+    ~semi_correct_env e -> 
+    Common_Sem.test_exceptions (` (` fps)) e lex = (b1, e1) -> 
+    Common_Sem.test_exceptions (` (` fps)) (normalise (` (` fps)) e) lex = (b2, e2) ->
+      get_trace e1 = get_trace e2 /\ b1 = b2.
+  Proof.
+    intros e lex. generalize dependent e. induction lex.
+    - simpl. intros e e1 b1 e2 b2 _ H1 H2. inversion H1; inversion H2; subst.
+      split; reflexivity.
+
+    - simpl. intros e e1 b1 e2 b2 Nsc.
+      destruct (Common_Sem.test_exception (` (` fps)) e a) as [b e'] eqn:Test1.
+      destruct (Common_Sem.test_exception (` (` fps)) (normalise (` (` fps)) e) a) as [b' e'1] eqn:Test2.
+      destruct (Incorrect_idb_test_exception_same_trace_normalise _ Nsc Test1 Test2).
+      subst.
+      destruct b'.
+      + intros H1 H2. inversion H1; inversion H2; subst. split; auto.
+      + have H1 := (normalise_through_test_exception_false _ _ Test1).
+        rewrite Test2 in H1. inversion H1. apply IHlex. 
+
+        unfold Common_Sem.test_exception in Test1.
+        destruct (get_expt_block_id a =? get_nav_block e).
+        * inversion Test1. subst. auto.
+        * unfold evalc in Test1. destruct (~~ EVAL_Def.eval (get_trace e) (get_expt_cond a));
+          inversion Test1.
+          apply Nsc.
+  Qed.
+
+  Lemma normalise_through_test_exceptions_false : forall e lex e',
+    Common_Sem.test_exceptions (` (` fps)) e lex = (false, e') ->
+    Common_Sem.test_exceptions (` (` fps)) (normalise (` (` fps)) e) lex = (false, (normalise (` (` fps)) e')).
+  Proof.
+    intros e lex. generalize dependent e. induction lex; simpl.
+    - intros e e' H. inversion H. reflexivity.
+    - intros e.
+      destruct (Common_Sem.test_exception (` (` fps)) e a) as [b e'] eqn:Test1.
+      destruct b; try by (intros; discriminate).
+      have Test2 := (normalise_through_test_exception_false _ _ Test1).
+      rewrite Test2. apply IHlex.
+  Qed.
+
+  Lemma Incorrect_idb_through_test_exceptions_false : forall e lex e',
+    ~semi_correct_env e ->
+    Common_Sem.test_exceptions (` (` fps)) e lex = (false, e') ->
+    ~semi_correct_env e'.
+  Proof.
+    intros e lex. generalize dependent e. induction lex; simpl.
+    - intros e e' Nsc H. inversion H. subst. auto.
+
+    - intros e e' Nsc.
+      destruct (Common_Sem.test_exception (` (` fps)) e a)
+      as [b e1] eqn:Test.
+      destruct b; try by (intros H; inversion H).
+      apply IHlex.
+      apply (Incorrect_idb_through_test_exception_false _ Nsc Test).
+  Qed.
+
+  Lemma Incorrect_idb_exception_same_trace_normalise : forall e e1 b1 e2 b2,
+    ~semi_correct_env e -> 
+    Common_Sem.exception (` (` fps)) e = (b1, e1) -> 
+    Common_Sem.exception (` (` fps)) (normalise (` (` fps)) e) = (b2, e2) ->
+      get_trace e1 = get_trace e2 /\ b1 = b2.
+  Proof.
+    unfold Common_Sem.exception. intros e e1 b1 e2 b2 Nsc.
+    destruct (Common_Sem.test_exceptions (` (` fps)) e (Common.get_fp_exceptions (` (` fps))))
+    as [b e'] eqn:Test1.
+    destruct (Common_Sem.test_exceptions (` (` fps)) (normalise (` (` fps)) e)
+    (Common.get_fp_exceptions (` (` fps))))
+    as [b' e''] eqn:Test2.
+    destruct (Incorrect_idb_test_exceptions_same_trace_normalise _ Nsc Test1 Test2).
+    subst.
+    destruct b'.
+    - intros H1 H2. inversion H1; inversion H2. subst. split; auto.
+    
+    - have H1 := (normalise_through_test_exceptions_false _ _ Test1).
+      rewrite Test2 in H1. inversion H1. subst. clear H1.
+      have Nsc' := (Incorrect_idb_through_test_exceptions_false _ Nsc Test1).
+      unfold semi_correct_env in Nsc'. unfold correct_block_id in Nsc'.
+      unfold get_nb_block in Nsc'. to_nat Nsc'.
+      unfold get_local_exceptions.
+      unfold get_current_block.
+      assert (FP_E.get_block (` (` fps)) (get_nav_block e') = get_default_block (` (` fps))).
+        apply get_block_default_block. unfold get_nb_block in *. unfold FPE_BS.fp.
+        ssrlia.
+      rewrite H0. simpl. clear H0.
+      assert (FP_E.get_block (` (` fps)) (FP_E.normalise_block_id (` (` fps)) (nav_block (get_state e'))) = get_default_block (` (` fps))).
+        unfold get_block. apply nth_overflow. unfold normalise_block_id.
+        unfold get_nb_block.
+        destruct ((Datatypes.length (FP_E.get_fp_blocks (` (` fps))) + 1)%coq_nat <=?
+        nav_block (get_state e'));
+        ssrlia.
+      rewrite H0. simpl. clear H0. 
+      intros H1 H2. inversion H1; inversion H2; subst. split; reflexivity.
+  Qed.
+  
+
   End FLIGHT_PLAN.
 
   Definition step_size (fps: flight_plan_sized) (e e': fp_env8) :=