From 133b5ad7ff8f9bff4c54e68444b88ae640faadb5 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 24 Nov 2023 16:55:49 +0100 Subject: [PATCH] Fixes after rebase --- erasure/theories/EImplementBox.v | 11 +++++------ erasure/theories/EInduction.v | 2 +- erasure/theories/EReflect.v | 6 +++--- quotation/theories/CommonUtils.v | 1 + .../ToPCUIC/QuotationOf/Common/Environment/Sig.v | 2 +- quotation/theories/ToTemplate/Init.v | 2 ++ .../ToTemplate/QuotationOf/Common/Environment/Sig.v | 2 +- 7 files changed, 14 insertions(+), 12 deletions(-) diff --git a/erasure/theories/EImplementBox.v b/erasure/theories/EImplementBox.v index 132539142..c5a3ad9fb 100644 --- a/erasure/theories/EImplementBox.v +++ b/erasure/theories/EImplementBox.v @@ -94,11 +94,11 @@ Section implement_box. rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?map_length; unfold test_def in *; simpl closed in *; - (*try solve [simpl; subst; simpl closed; f_equal; auto; rtoProp; solve_all; solve_all]; try easy. + try solve [simpl; subst; simpl closed; f_equal; auto; rtoProp; solve_all; solve_all]; try easy. rtoProp. split. eauto. solve_all. replace (#|x.1| + S k) with (#|x.1| + k + 1) by lia. - eapply closedn_lift. eauto.*) + eapply closedn_lift. eauto. try solve [simpl; subst; simpl closed; f_equal; auto; rtoProp; solve_all; solve_all_k 6]; try easy. Qed. @@ -124,10 +124,9 @@ Section implement_box. f_equal. lia. - cbn. f_equal. rewrite !map_map. solve_all. eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. erewrite H; eauto. - f_equal. now rewrite map_length. - cbn. f_equal. rewrite !map_map. solve_all. eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. erewrite H; eauto. - f_equal. now rewrite map_length. + - solve_all_k 6. Qed. (* Lemma implement_box_subst a k b : *) @@ -185,9 +184,9 @@ Section implement_box. f_equal. eapply H; eauto. - cbn. f_equal. rewrite !map_map. solve_all. - eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. rewrite H; eauto. + eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. solve_all. - cbn. f_equal. rewrite !map_map. solve_all. - eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. rewrite H; eauto. + eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. solve_all. - cbn. solve_all. Qed. diff --git a/erasure/theories/EInduction.v b/erasure/theories/EInduction.v index 208332ffc..306b6d25c 100644 --- a/erasure/theories/EInduction.v +++ b/erasure/theories/EInduction.v @@ -67,7 +67,7 @@ Proof. destruct mfix; constructor; [|apply auxm]. apply auxt. - destruct p as [? []]; cbn => //; constructor. + destruct prim as [? []]; cbn => //; constructor. destruct a as [def v]; cbn. split. eapply auxt. revert v; fix auxv 1. diff --git a/erasure/theories/EReflect.v b/erasure/theories/EReflect.v index 9fbc550b8..71284edc2 100644 --- a/erasure/theories/EReflect.v +++ b/erasure/theories/EReflect.v @@ -112,13 +112,13 @@ Proof. subst. inversion e0. subst. destruct (eq_dec rarg rarg0) ; nodec. subst. left. reflexivity. - - destruct p as [? []]; destruct p0 as [? []]; cbn ; nodec. + - destruct prim as [? []]; destruct p as [? []]; cbn ; nodec. + destruct (eq_dec i i0); nodec; subst; eauto. + destruct (eq_dec f f0); nodec; subst; eauto. + destruct a as [? ?], a0 as [? ?]; cbn. depelim X. destruct p as [hd hv]. cbn in *. - destruct (hd array_default0); nodec; subst; eauto. - revert array_value0; induction hv; intros []; eauto; nodec. + destruct (hd array_default); nodec; subst; eauto. + revert array_value; induction hv; intros []; eauto; nodec. destruct (p t); subst; nodec. destruct (IHhv l0); nodec. noconf e; eauto. Defined. diff --git a/quotation/theories/CommonUtils.v b/quotation/theories/CommonUtils.v index 18943d44e..27f703c07 100644 --- a/quotation/theories/CommonUtils.v +++ b/quotation/theories/CommonUtils.v @@ -188,6 +188,7 @@ Module WithTemplate. | tVar _ | tInt _ | tFloat _ + | tArray _ _ _ _ | tConst _ _ | tInd _ _ | tConstruct _ _ _ diff --git a/quotation/theories/ToPCUIC/QuotationOf/Common/Environment/Sig.v b/quotation/theories/ToPCUIC/QuotationOf/Common/Environment/Sig.v index 31de3ebc0..3b5d13ea9 100644 --- a/quotation/theories/ToPCUIC/QuotationOf/Common/Environment/Sig.v +++ b/quotation/theories/ToPCUIC/QuotationOf/Common/Environment/Sig.v @@ -43,7 +43,7 @@ Module Type QuoteEnvironmentSig (T : Term) (Import E : EnvironmentSig T). #[export] Declare Instance quote_extends {Σ Σ'} : ground_quotable (@extends Σ Σ'). #[export] Declare Instance quote_extends_decls {Σ Σ'} : ground_quotable (@extends_decls Σ Σ'). - #[export] Declare Instance quote_primitive_invariants {cdecl} : ground_quotable (primitive_invariants cdecl). + #[export] Declare Instance quote_primitive_invariants {cdecl ty} : ground_quotable (primitive_invariants cdecl ty). #[export] Declare Instance quote_All_decls {P t t'} {qP : quotation_of P} {quoteP : forall t t', ground_quotable (P t t')} : ground_quotable (All_decls P t t'). #[export] Declare Instance quote_All_decls_alpha {P t t'} {qP : quotation_of P} {quoteP : forall t t', ground_quotable (P t t')} : ground_quotable (All_decls_alpha P t t'). diff --git a/quotation/theories/ToTemplate/Init.v b/quotation/theories/ToTemplate/Init.v index 4bf46f2f7..487ea21ba 100644 --- a/quotation/theories/ToTemplate/Init.v +++ b/quotation/theories/ToTemplate/Init.v @@ -108,6 +108,7 @@ Proof. | tSort _ | tInt _ | tFloat _ + | tArray _ _ _ _ | tConst _ _ => if head_term_is_bound cur_modpath qt then tmMaybeInferQuotation tt @@ -212,6 +213,7 @@ Proof. | tConstruct _ _ _ | tInt _ | tFloat _ + | tArray _ _ _ _ | tInd _ _ => ret qt | tCast t kind v diff --git a/quotation/theories/ToTemplate/QuotationOf/Common/Environment/Sig.v b/quotation/theories/ToTemplate/QuotationOf/Common/Environment/Sig.v index 7bfba4ce3..86e7a9309 100644 --- a/quotation/theories/ToTemplate/QuotationOf/Common/Environment/Sig.v +++ b/quotation/theories/ToTemplate/QuotationOf/Common/Environment/Sig.v @@ -43,7 +43,7 @@ Module Type QuoteEnvironmentSig (T : Term) (Import E : EnvironmentSig T). #[export] Declare Instance quote_extends {Σ Σ'} : ground_quotable (@extends Σ Σ'). #[export] Declare Instance quote_extends_decls {Σ Σ'} : ground_quotable (@extends_decls Σ Σ'). - #[export] Declare Instance quote_primitive_invariants {cdecl} : ground_quotable (primitive_invariants cdecl). + #[export] Declare Instance quote_primitive_invariants {cdecl ty} : ground_quotable (primitive_invariants cdecl ty). #[export] Declare Instance quote_All_decls {P t t'} {qP : quotation_of P} {quoteP : forall t t', ground_quotable (P t t')} : ground_quotable (All_decls P t t'). #[export] Declare Instance quote_All_decls_alpha {P t t'} {qP : quotation_of P} {quoteP : forall t t', ground_quotable (P t t')} : ground_quotable (All_decls_alpha P t t').