Merge pull request #468 from kyoDralliam/conversion-completeness

Conversion completeness

.gitignore

@@ -397,6 +397,9 @@ vs.mli
 *.v.timing
 time-of-build.log
 time-of-build-pretty.log
+_build/**
+extraction/src/*.ml
+extraction/src/*.mli
 erasure/src/orderedTypeAlt.ml
 erasure/src/orderedTypeAlt.mli
 erasure/src/orderedTypeEx.ml

erasure/_PluginProject.in

@@ -81,8 +81,6 @@ src/pCUICChecker.ml
 src/pCUICChecker.mli
 src/pCUICPretty.mli
 src/pCUICPretty.ml
-src/pCUICSafeLemmata.mli
-src/pCUICSafeLemmata.ml
 src/templateToPCUIC.mli
 src/templateToPCUIC.ml
 
@@ -126,4 +124,4 @@ src/safeTemplateErasure.ml
 src/g_metacoq_erasure.mlg
 src/metacoq_erasure_plugin.mlpack
 
-theories/Loader.v
+theories/Loader.v

erasure/src/metacoq_erasure_plugin.mlpack

@@ -31,7 +31,6 @@ PCUICChecker
 PCUICPretty
 PCUICRetyping
 TemplateToPCUIC
-PCUICSafeLemmata
 PCUICCumulativity
 
 PCUICUnivSubst

erasure/theories/EArities.v

@@ -310,120 +310,6 @@ Proof.
   - eexists _, _; intuition eauto.
 Qed.
 
-Inductive conv_decls (Σ : global_env_ext) Γ (Γ' : context) : forall (x y : context_decl), Type :=
-| conv_vass : forall (na na' : name) (T T' : term),
-                (* isWfArity_or_Type Σ Γ' T' -> *)
-                Σ;;; Γ |- T = T' -> conv_decls Σ Γ Γ' (vass na T) (vass na' T')
-| conv_vdef_type : forall (na : name) (b T  : term),
-    (* isWfArity_or_Type Σ Γ' T -> *)
-    conv_decls Σ Γ Γ' (vdef na b T) (vdef na b T).
-
-Lemma conv_context_refl (Σ : global_env_ext) Γ :
-  wf Σ -> wf_local Σ Γ ->
-  context_relation (@conv_decls Σ) Γ Γ.
-Proof.
-  induction Γ; try econstructor.
-  intros wfΣ wfΓ; depelim wfΓ; econstructor; eauto;
-  constructor; auto.
-Qed.
-
-Lemma context_conversion_red1 (Σ : global_env_ext) Γ Γ' s t : wf Σ -> (* Σ ;;; Γ' |- t : T -> *)
-   context_relation (@conv_decls Σ) Γ Γ' -> red1 Σ Γ s t -> red Σ Γ' s t.
-Proof.
-  intros HΣ HT X0. induction X0 using red1_ind_all in Γ', HΣ, HT |- *; eauto.
-  all:pcuic.
-  - econstructor. econstructor.
-    rewrite <- H.
-    induction HT in i |- *; destruct i; eauto.
-    now inv p.
-  -
-    eapply PCUICReduction.red_abs. eapply IHX0; eauto.  eauto.
-  -
-    eapply PCUICReduction.red_abs. eauto. eapply IHX0. eauto.
-    eauto. econstructor. eauto. econstructor.
-    eapply PCUICCumulativity.conv_refl'.
-  -
-    eapply PCUICReduction.red_letin. eapply IHX0; eauto.
-    all:eauto.
-  -
-    eapply PCUICReduction.red_letin; eauto.
-  -
-    eapply PCUICReduction.red_letin; eauto. eapply IHX0; eauto.
-    econstructor. eauto. econstructor.
-  -     eapply PCUICReduction.red_case; eauto. clear.
-    eapply All_All2_refl. induction brs; eauto.
-  -     eapply PCUICReduction.red_case; eauto. clear.
-    eapply All_All2_refl. induction brs; eauto.
-  - destruct a.
-    eapply red_case; eauto.
-    clear - HΣ X HT.
-    induction X.
-    + econstructor. destruct p. destruct p.
-      split; eauto.
-      eapply All_All2_refl.
-      induction tl; eauto.
-    + econstructor. now split.
-      eassumption.
-  -
-    eapply PCUICReduction.red_proj_c. eauto.
-  -
-    eapply PCUICReduction.red_app; eauto.
-  -     eapply PCUICReduction.red_app; eauto.
-  -
-    eapply PCUICReduction.red_prod; eauto.
-  -
-    eapply PCUICReduction.red_prod; eauto. eapply IHX0. eauto. eauto.
-    econstructor.
-    eauto. econstructor. eapply PCUICCumulativity.conv_refl'.
-  - eapply PCUICReduction.red_evar; eauto.
-    induction X; eauto. econstructor. eapply p; eauto.
-    induction tl; eauto.
-  - eapply PCUICReduction.red_fix_one_ty.
-    eapply OnOne2_impl ; eauto.
-    intros [? ? ? ?] [? ? ? ?] [[r ih] e]. simpl in *.
-    inversion e. subst. clear e.
-    split ; auto.
-  - eapply PCUICReduction.red_fix_one_body.
-    eapply OnOne2_impl ; eauto.
-    intros [? ? ? ?] [? ? ? ?] [[r ih] e]. simpl in *.
-    inversion e. subst. clear e.
-    split ; auto.
-    eapply ih ; auto.
-    clear - HT.
-    induction (fix_context mfix0) as [| [na [b|] ty] Δ ihΔ].
-    + auto.
-    + simpl. constructor ; eauto.
-      constructor.
-    + simpl. constructor ; eauto.
-      constructor. apply PCUICCumulativity.conv_refl'.
-  - eapply PCUICReduction.red_cofix_one_ty.
-    eapply OnOne2_impl ; eauto.
-    intros [? ? ? ?] [? ? ? ?] [[r ih] e]. simpl in *.
-    inversion e. subst. clear e.
-    split ; auto.
-  - eapply PCUICReduction.red_cofix_one_body.
-    eapply OnOne2_impl ; eauto.
-    intros [? ? ? ?] [? ? ? ?] [[r ih] e]. simpl in *.
-    inversion e. subst. clear e.
-    split ; auto.
-    eapply ih ; auto.
-    clear - HT.
-    induction (fix_context mfix0) as [| [na [b|] ty] Δ ihΔ].
-    + auto.
-    + simpl. constructor ; eauto.
-      constructor.
-    + simpl. constructor ; eauto.
-      constructor. apply PCUICCumulativity.conv_refl'.
-Qed.
-
-Lemma context_conversion_red (Σ : global_env_ext) Γ Γ' s t : wf Σ ->
-  context_relation (@conv_decls Σ) Γ Γ' -> red Σ Γ s t -> red Σ Γ' s t.
-Proof.
-  intros. induction X1 using red_rect'; eauto.
-  etransitivity. eapply IHX1.
-  eapply context_conversion_red1; eauto.
-Qed.
-
 Lemma isWfArity_or_Type_red:
   forall (Σ : global_env_ext) (Γ : context) (T : term), wf Σ -> wf_local Σ Γ ->
     isWfArity_or_Type Σ Γ T -> forall x5 : term, red Σ Γ T x5 -> isWfArity_or_Type Σ Γ x5.
@@ -627,4 +513,4 @@ Proof.
   exists u; split; auto.
   eapply cumul_prop2; eauto. eapply PCUICValidity.validity; eauto.
   eapply cumul_prop1; eauto. eapply PCUICValidity.validity; eauto.
-Qed.
+Qed.

erasure/theories/ErasureCorrectness.v

@@ -79,7 +79,7 @@ Lemma wf_local_rel_conv:
   forall Σ : global_env × universes_decl,
     wf Σ.1 ->
     forall Γ Γ' : context,
-      PCUICContextConversion.context_relation (PCUICContextConversion.conv_decls Σ) Γ Γ' ->
+      PCUICContextRelation.context_relation (PCUICContextConversion.conv_decls Σ) Γ Γ' ->
       forall Γ0 : context, wf_local Σ Γ' -> wf_local_rel Σ Γ Γ0 -> wf_local_rel Σ Γ' Γ0.
 Proof.
   intros Σ wfΣ Γ Γ' X1 Γ0 ? w0. induction w0.

erasure/theories/ErasureFunction.v

@@ -127,10 +127,12 @@ Defined.
 Next Obligation.
   pose proof (hnf_sound HΣ (h := h)).
   repeat match goal with [H : squash (red _ _ _ _ ) |- _ ] => destruct H end.
-  destruct HΣ.
+  destruct H, HΣ.
   eapply PCUICConfluence.red_confluence in X0 as [t'' []]. 3:exact X1. 2:eauto.
   eapply invert_red_sort in r0; eauto. subst.
-  eapply whnf_red_sort in r. congruence. eauto.
+  eapply whnf_red_inv in r; auto.
+  depelim r.
+  congruence.
 Qed.
 
 Program Definition reduce_to_prod' Γ t (h : wellformed Σ Γ t)
@@ -150,10 +152,12 @@ Defined.
 Next Obligation.
   pose proof (hnf_sound HΣ (h := h)).
   repeat match goal with [H : squash (red _ _ _ _ ) |- _ ] => destruct H end.
-  destruct HΣ.
+  destruct H, HΣ.
   eapply PCUICConfluence.red_confluence in X2 as [t'' []]. 3:exact X3. 2:eauto.
   eapply invert_red_prod in r0 as (? & ? & [] & ?); eauto. subst.
-  eapply whnf_red_prod in r as (? & ? & ?). congruence. eauto.
+  eapply whnf_red_inv in r; auto.
+  depelim r.
+  congruence.
 Qed.
 
 Equations is_arity Γ (HΓ : ∥wf_local Σ Γ∥) T (HT : wellformed Σ Γ T) :
@@ -221,23 +225,13 @@ Next Obligation.
   eapply invert_red_prod in X2 as (? & ? & [] & ?); eauto. subst. cbn in *.
   exists x4; split; eauto.
 
-  destruct HT as [ [] | [] ].
-  ++ sq. etransitivity; eauto.
-     eapply context_conversion_red; eauto. econstructor.
-
-     eapply conv_context_refl; eauto. econstructor.
-
-     eapply conv_sym, red_conv; eauto.
-
-  ++ sq. etransitivity. eassumption.
-
-     eapply context_conversion_red; eauto. econstructor.
-
-     eapply conv_context_refl; eauto.
-
-     econstructor.
-
-     eapply conv_sym, red_conv; eauto.
+  constructor.
+  etransitivity; eauto.
+  eapply PCUICContextRelation.context_change_decl_types_red; eauto.
+  constructor; [|constructor].
+  eapply PCUICContextRelation.context_relation_refl.
+  intros.
+  reflexivity.
 Qed.
 
 Hint Constructors squash : core.

erasure/theories/SafeErasureFunction.v

@@ -185,32 +185,13 @@ Section fix_sigma.
 
     eapply invert_red_prod in X2 as (? & ? & [] & ?); eauto. subst. cbn in *.
     exists x4; split; eauto.
-
-    destruct HT as [ [] | [] ].
-    ++ sq. pose proof t. pose proof t.
-
-      eapply subject_reduction in X3. 2:eauto. 2:{ etransitivity. exact X. exact r0. }
-      eapply inversion_Prod in X3 as (? & ? & ? & ? & ?) ; auto.
-
-      eapply subject_reduction in X2. 2:eauto. 2:{ exact X0. }
-      eapply inversion_Prod in X2 as (? & ? & ? & ? & ?) ; auto.
-
-      etransitivity. eassumption.
-
-      eapply context_conversion_red; eauto. econstructor.
-
-      eapply conv_context_refl; eauto. econstructor.
-
-      eapply conv_sym, red_conv; eauto.
-    ++ sq. etransitivity. eassumption.
-
-      eapply context_conversion_red; eauto. econstructor.
-
-      eapply conv_context_refl; eauto.
-
-      econstructor.
-
-      eapply conv_sym, red_conv; eauto.
+
+    constructor.
+    etransitivity; eauto.
+    eapply PCUICContextRelation.context_change_decl_types_red; eauto.
+    constructor; [|constructor].
+    eapply PCUICContextRelation.context_relation_refl.
+    reflexivity.
   Qed.
 
   Next Obligation.

pcuic/_CoqProject.in

@@ -25,8 +25,10 @@ theories/PCUICReduction.v
 theories/PCUICParallelReduction.v
 theories/PCUICParallelReductionConfluence.v
 theories/PCUICConfluence.v
+theories/PCUICContextRelation.v
 theories/PCUICContextConversion.v
 theories/PCUICConversion.v
+theories/PCUICConvCumInversion.v
 theories/PCUICGeneration.v
 theories/PCUICAlpha.v
 theories/PCUICCtxShape.v

pcuic/theories/PCUICCanonicity.v

@@ -1030,7 +1030,7 @@ Section WeakNormalization.
     - clear wh_neutral_empty_gen wh_normal_empty_gen. subst.
       apply inversion_Const in typed as [decl' [wfd [declc [cu cum]]]]; eauto.
       specialize (axfree  _ _ declc).
-      red in declc. rewrite declc in H. noconf H. congruence.
+      red in declc. rewrite declc in e. noconf e. congruence.
     - simpl in cl; move/andP: cl => [clf cla].
       eapply inversion_App in typed as [na [A [B [Hf _]]]]; eauto.
     - specialize (wh_neutral_empty_gen _ _ axfree ne). subst.
@@ -1039,15 +1039,15 @@ Section WeakNormalization.
       eapply inversion_Fix in t as (? & ? & ? & ? & ? & ? & ?); auto.
       eapply typing_spine_strengthen in t0; eauto.
       eapply nth_error_all in a; eauto. simpl in a.
-      rewrite /unfold_fix in H. rewrite e in H. noconf H.
+      rewrite /unfold_fix in e. rewrite e1 in e. noconf e.
       eapply (wf_fixpoint_spine wfΣ) in t0; eauto.
-      rewrite H0 in t0. destruct t0 as [ind [u [indargs [tyarg ckind]]]].
+      rewrite e0 in t0. destruct t0 as [ind [u [indargs [tyarg ckind]]]].
       clear wh_normal_empty_gen.
       now specialize (wh_neutral_empty_gen _ tyarg eq_refl).
     - move/andP: cl => [/andP[_ clc] _].
       eapply inversion_Case in typed; firstorder eauto.
     - eapply inversion_Proj in typed; firstorder auto.
-    - eapply wh_neutral_empty_gen in H; eauto.
+    - eapply wh_neutral_empty_gen in w; eauto.
     - eapply inversion_Sort in typed as (? & ? & ? & ? & ?); auto.
       eapply invert_cumul_sort_l in c as (? & ? & ?); auto.
       eapply red_mkApps_tInd in r as (? & eq & ?); eauto; eauto.