Proof of forbidden_deroute_NEC Lemma

src/verification/CommonFPVerification.v

@@ -3090,18 +3090,70 @@ Section No_External_Call_FP.
             -- (** induction *) apply IHf0. }
   Qed.
 
-  Lemma forbidden_deroute_NEC : forall fpe,
-    No_external_call_statement (fn_body (gen_fp_forbidden_deroute fpe)).
-  Admitted.
-  
-
   Ltac autoProov_NEC_f := repeat (try constructor;
     try apply parse_c_code_NEC;
     try apply gen_fun_call_stmt_NEC;
     try apply gen_fp_pitch_NEC;
     try apply gen_fp_vmode_NEC;
     try apply gen_fp_hmode_NEC ).
+
+    Lemma pn_le_m : forall n m p,
+      (p + m)%coq_nat <= n -> m <= n.
+    Proof.
+      intros n. induction n.
+      - intros m. destruct m.
+        + simpl. intros p _. auto.
+        + simpl. intros p H. rewrite Nat.add_succ_r in H. auto.
+      - intros m. destruct m.
+        + auto.
+        + intros p H. rewrite ltnS. apply IHn with p. rewrite Nat.add_succ_r in H.
+          rewrite ltnS in H. apply H. 
+    Qed.
   
+  Lemma aux_forbidden_deroute_NEC : forall n fpe,
+    length fpe < n ->
+    No_external_call_statement_labeled (gen_forbidden_deroute_case fpe (LScons None Sbreak LSnil)).
+  Proof.
+    intros n. 
+    induction n.
+    - intros fpe H. destruct fpe. 
+      rewrite gen_forbidden_deroute_case_equation.
+      autoProov_NEC_f.
+      simpl in H. inversion H.
+    - intros fpe H. destruct fpe; simpl in *.
+      + rewrite gen_forbidden_deroute_case_equation.
+        autoProov_NEC_f.
+      + rewrite gen_forbidden_deroute_case_equation.
+        remember (partition (test_from (get_fbd_from f0)) (f0 :: fpe0)) as partres.
+        destruct partres.
+        autoProov_NEC_f. destruct Heqpartres.
+        induction l. 
+        * autoProov_NEC_f.
+        * simpl. autoProov_NEC_f.
+          -- destruct (get_fbd_only_when a); autoProov_NEC_f.
+          -- apply IHl.
+        apply IHn. symmetry in Heqpartres.
+        simpl in Heqpartres. rewrite test_from_refl in Heqpartres.
+        remember (partition (test_from (get_fbd_from f0)) fpe0) as temp.
+        destruct temp; subst. inversion Heqpartres. subst.
+        symmetry in Heqtemp. 
+        apply partition_length in Heqtemp. rewrite Heqtemp in H.
+        clear Heqpartres. clear Heqtemp. clear IHn.
+        remember (Datatypes.length l1) as p. 
+        remember (Datatypes.length l0) as m.
+        apply ltnSE in H. 
+        destruct n. inversion H.
+        rewrite ltnS. rewrite ltnS in H.
+        apply pn_le_m in H. apply H.
+  Qed.
+
+  Lemma forbidden_deroute_NEC : forall fpe,
+    No_external_call_statement (fn_body (gen_fp_forbidden_deroute fpe)).
+  Proof.
+    simpl. autoProov_NEC_f. 
+    apply aux_forbidden_deroute_NEC with ((Datatypes.length (FP_E.get_fp_forbidden_deroutes fpe0)).+1).
+    apply ltnSn.
+  Qed.
   
   Lemma No_function_in_gvars: forall ident0 f0,
     ~ (In (ident0, Gfun f0) (` gvars)%list).