Proof that reordering of constructors is correct (#1095)

* WIP on reordering constructors

* New/old tag reasoning

* WIP correctness of constructor reordering. main lemma proven

* Reordering preserves well-formedness

* Reorderin

* Admit free proofs of preservation for wf and substitution

* WIP adapting to an additional mapping argument for transforms and stronger wellformedness property on extracted terms

* Full composed pipeline with mapping of constructors

* Fixes due to removal of useless -fast flag and change for reordering of constructors, now verified

* Remove option to reorder constructors, now safely done always

* Fix metacoq_tour

* Fix a remaining todo

* Remove generated files

.vscode/metacoq.code-workspace

@@ -106,5 +106,6 @@
 		"**/.DS_Store": true,
 		"**/Thumbs.db": true
 	},
+	"coq-lsp.check_only_on_request": true,
   }
 }

erasure-plugin/clean_extraction.sh

@@ -9,7 +9,7 @@ fi
 
 shopt -s nullglob # make the for loop do nothnig when there is no *.ml* files
 
-files=`cat ../template-coq/_PluginProject | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
+files=`cat ../template-coq/_PluginProject.in | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
 
 if [[ ! -f "src/metacoq_erasure_plugin.cmxs" ||
            "src/metacoq_erasure_plugin.cmxs" -ot "theories/Extraction.vo" ]]

erasure-plugin/src/g_metacoq_erasure.mlg

@@ -25,7 +25,6 @@ type erasure_command_args =
   | Time
   | Typed
   | BypassQeds
-  | Fast
 
 let pr_char c = str (Char.escaped c)
 
@@ -46,24 +45,19 @@ type erasure_config =
   { unsafe : bool;
     time : bool;
     typed : bool;
-    bypass_qeds : bool;
-    fast : bool;
-    }
+    bypass_qeds : bool }
 
 let default_config =
   { unsafe = false;
     time = false;
     typed = false;
-    bypass_qeds = false;
-    fast = false }
+    bypass_qeds = false }
 
 let make_erasure_config config =
   let open Erasure0 in
   { enable_unsafe = if config.unsafe then all_unsafe_passes else no_unsafe_passes ;
     enable_typed_erasure = config.typed;
-    enable_fast_remove_params = config.fast;
     dearging_config = default_dearging_config;
-    inductives_mapping = [];
     inlined_constants = Kernames.KernameSet.empty }
 
 let time_opt config str fn arg =
@@ -76,8 +70,9 @@ let check config env evm c =
   let time str f arg = time_opt config str f arg in
   let term = time (str"Quoting") (Ast_quoter.quote_term_rec ~bypass:config.bypass_qeds env evm) (EConstr.to_constr evm c) in
   let erasure_config = make_erasure_config config in
+  let mapping = [] in
   let erase =
-    time (str"Erasure") (Erasure0.erase_and_print_template_program erasure_config) term
+    time (str"Erasure") (Erasure0.erase_and_print_template_program erasure_config mapping) term
   in
   Feedback.msg_notice (pr_char_list erase)
 
@@ -92,7 +87,6 @@ let interp_erase args env evm c =
         | Time -> aux {config with time = true} args
         | Typed -> aux {config with typed = true} args
         | BypassQeds -> aux {config with bypass_qeds = true} args
-        | Fast -> aux {config with fast = true} args
     in aux default_config args
   in
   check config env evm c
@@ -123,7 +117,6 @@ ARGUMENT EXTEND erase_args
 | [ "-time" ] -> { Time }
 | [ "-typed" ] -> { Typed }
 | [ "-bypass-qeds" ] -> { BypassQeds }
-| [ "-fast" ] -> { Fast }
 END
 
 VERNAC COMMAND EXTEND MetaCoqErase CLASSIFIED AS QUERY

erasure-plugin/theories/ETransform.v

@@ -1020,42 +1020,59 @@ Qed.
 
 From MetaCoq.Erasure Require Import EReorderCstrs.
 
-Axiom trust_reorder_cstrs_wf :
-  forall efl : EEnvFlags,
-  WcbvFlags ->
-  forall (m : inductives_mapping) (input : Transform.program E.global_context term),
-  wf_eprogram efl input -> wf_eprogram efl (reorder_program m input).
-Axiom trust_reorder_cstrs_pres :
-  forall (efl : EEnvFlags) (wfl : WcbvFlags) (m : inductives_mapping) (p : Transform.program E.global_context term)
-  (v : term),
-  wf_eprogram efl p ->
-  eval_eprogram wfl p v -> exists v' : term, eval_eprogram wfl (reorder_program m p) v' /\ v' = reorder m v.
+Definition eval_eprogram_mapping (wfl : WcbvFlags) (p : inductives_mapping * eprogram) t :=
+  eval_eprogram wfl p.2 t.
 
-Program Definition reorder_cstrs_transformation (efl : EEnvFlags) (wfl : WcbvFlags) (m : inductives_mapping) :
-  Transform.t _ _ EAst.term EAst.term _ _
-    (eval_eprogram wfl) (eval_eprogram wfl) :=
-  {| name := "reoder inductive constructors ";
-    transform p _ := EReorderCstrs.reorder_program m p ;
-    pre p := wf_eprogram efl p ;
-    post p := wf_eprogram efl p ;
-    obseq p hp p' v v' := v' = EReorderCstrs.reorder m v |}.
+Definition eval_eprogram_env_mapping (wfl : WcbvFlags) (p : inductives_mapping * eprogram_env) t :=
+  eval_eprogram_env wfl p.2 t.
+
+Definition to_program (e : eprogram_env) : eprogram :=
+  (e.1, e.2).
+
+Program Definition reorder_cstrs_transformation {efl : EEnvFlags} {wca : cstr_as_blocks = false} {has_app : has_tApp}
+  (wfl : WcbvFlags) {wcon : with_constructor_as_block = false} :
+  Transform.t _ _ _ EAst.term _ _
+    (eval_eprogram_env_mapping wfl) (eval_eprogram wfl) :=
+  {| name := "reorder inductive constructors ";
+    transform p _ := EReorderCstrs.reorder_program p.1 (to_program p.2) ;
+    pre p := [/\ wf_eprogram_env efl p.2, EEtaExpandedFix.expanded_eprogram_env p.2 & wf_inductives_mapping p.2.1 p.1] ;
+    post p := wf_eprogram efl p /\ EEtaExpandedFix.expanded_eprogram p;
+    obseq p hp p' v v' := v' = EReorderCstrs.reorder p.1 v |}.
 
 Next Obligation.
-  move=> efl wfl m. cbn. now apply trust_reorder_cstrs_wf.
+  move=> efl wca hasapp wfl wcb [m p] [wfp exp wfm]. split => //.
+  now unshelve eapply reorder_program_wf. cbn.
+  now eapply reorder_program_expanded_fix.
 Qed.
 Next Obligation.
-  red. eapply trust_reorder_cstrs_pres.
+  red. intros efl wca hasapp wfl wcb [m p] v [wfp wfm] evp.
+  destruct evp as [ev].
+  unshelve eapply EReorderCstrs.optimize_correct in ev; trea.
+  2,3:apply wfp.
+  exists (reorder m v). split => //.
 Qed.
 
 #[global]
-Axiom trust_reorder_cstrs_transformation_ext : forall (efl : EEnvFlags) (wfl : WcbvFlags) (m : inductives_mapping),
-  TransformExt.t (reorder_cstrs_transformation efl wfl m)
-    (fun p p' => extends p.1 p'.1) (fun p p' => extends p.1 p'.1).
+Instance reorder_cstrs_transformation_ext {efl : EEnvFlags} (wca : cstr_as_blocks = false) (has_app : has_tApp) (wfl : WcbvFlags)
+  {wcon : with_constructor_as_block = false} :
+  TransformExt.t (reorder_cstrs_transformation (wca := wca) (has_app := has_app) wfl (wcon:=wcon))
+    (fun p p' => p.1 = p'.1 /\ extends p.2.1 p'.2.1) (fun p p' => extends p.1 p'.1).
+Proof.
+  red. intros p p' pr pr' [eq ext].
+  red; cbn. rewrite -eq. eapply EReorderCstrs.optimize_extends_env; eauto.
+  move: pr'; cbn. now intros []. apply pr. apply pr'.
+Qed.
 
 #[global]
-Axiom trust_reorder_cstrs_transformation_ext' : forall (efl : EEnvFlags) (wfl : WcbvFlags) (m : inductives_mapping),
-  TransformExt.t (reorder_cstrs_transformation efl wfl m)
-    extends_eprogram extends_eprogram.
+Instance reorder_cstrs_transformation_ext' {efl : EEnvFlags} (wca : cstr_as_blocks = false) (has_app : has_tApp) (wfl : WcbvFlags)
+  {wcon : with_constructor_as_block = false} :
+  TransformExt.t (reorder_cstrs_transformation (wca := wca) (has_app := has_app) wfl (wcon:=wcon))
+    (fun p p' => p.1 = p'.1 /\ extends_eprogram_env p.2 p'.2) extends_eprogram.
+Proof.
+  red. intros p p' pr pr' [eq [ext eq']]. cbn.
+  red. cbn. rewrite -eq -eq'. split => //. eapply EReorderCstrs.optimize_extends_env; eauto.
+  move: pr'; cbn. now intros []. apply pr. apply pr'.
+Qed.
 
 From MetaCoq.Erasure Require Import EUnboxing.