diff options
Diffstat (limited to 'src/Reflection')
48 files changed, 263 insertions, 263 deletions
diff --git a/src/Reflection/BoundByCastInterp.v b/src/Reflection/BoundByCastInterp.v index cf6131a5e..46a50fd42 100644 --- a/src/Reflection/BoundByCastInterp.v +++ b/src/Reflection/BoundByCastInterp.v @@ -103,7 +103,7 @@ Section language. -> is_bounded_by (Interp interp_op e (interpf_smart_unbound input_bounds x)) output_bounds /\ interpf_smart_unbound _ (Interp interp_op e' x) = Interp interp_op e (interpf_smart_unbound input_bounds x). - Proof. + Proof using cast_val_squash interpf_Cast_id interpf_bound_op interpf_cast is_bounded_by_bound_op is_bounded_by_interp_op is_cast_correct strip_cast_val wff_Cast. intros; subst e' output_bounds. unfold Boundify. erewrite InterpExprEta, InterpInlineCast, InterpLinearize by eauto with wf. diff --git a/src/Reflection/BoundByCastWf.v b/src/Reflection/BoundByCastWf.v index f192fb06d..cc60f14b1 100644 --- a/src/Reflection/BoundByCastWf.v +++ b/src/Reflection/BoundByCastWf.v @@ -39,7 +39,7 @@ Section language. Cast is_cast is_const genericize_op failf t1 e1 args2). - Proof. + Proof using wff_Cast. unfold Boundify; auto 7 with wf. Qed. End language. diff --git a/src/Reflection/Conversion.v b/src/Reflection/Conversion.v index 8d2250a7a..bd0f4f695 100644 --- a/src/Reflection/Conversion.v +++ b/src/Reflection/Conversion.v @@ -44,7 +44,7 @@ Section language. (fun _ x => x) (fun _ x => x) t e = e. - Proof. + Proof using functional_extensionality. induction e; repeat match goal with | _ => reflexivity @@ -82,7 +82,7 @@ Section language. f_var12 f_var21 t e) = interpf interp_op e. - Proof. + Proof using f_var12_id f_var21_id. induction e; repeat match goal with | _ => progress unfold LetIn.Let_In diff --git a/src/Reflection/EtaInterp.v b/src/Reflection/EtaInterp.v index 4ab42a63f..deb551d7d 100644 --- a/src/Reflection/EtaInterp.v +++ b/src/Reflection/EtaInterp.v @@ -33,7 +33,7 @@ Section language. (eq_eta : forall A B x, @eta A B x = x). Lemma eq_interp_flat_type_eta_gen {var t T f} x : @interp_flat_type_eta_gen base_type_code var eta t T f x = f x. - Proof. induction t; t. Qed. + Proof using eq_eta. induction t; t. Qed. (* Local *) Hint Rewrite @eq_interp_flat_type_eta_gen. @@ -43,17 +43,17 @@ Section language. Lemma interp_expr_eta_gen {t e} : forall x, interp (@interp_op) (expr_eta_gen eta exprf_eta (t:=t) e) x = interp (@interp_op) e x. - Proof. t. Qed. + Proof using Type*. t. Qed. End gen_type. (* Local *) Hint Rewrite @interp_expr_eta_gen. Lemma interpf_exprf_eta_gen {t e} : interpf (@interp_op) (exprf_eta_gen eta (t:=t) e) = interpf (@interp_op) e. - Proof. induction e; t. Qed. + Proof using eq_eta. induction e; t. Qed. Lemma InterpExprEtaGen {t e} : forall x, Interp (@interp_op) (ExprEtaGen eta (t:=t) e) x = Interp (@interp_op) e x. - Proof. apply interp_expr_eta_gen; intros; apply interpf_exprf_eta_gen. Qed. + Proof using eq_eta. apply interp_expr_eta_gen; intros; apply interpf_exprf_eta_gen. Qed. End gen_flat_type. (* Local *) Hint Rewrite @eq_interp_flat_type_eta_gen. (* Local *) Hint Rewrite @interp_expr_eta_gen. @@ -61,45 +61,45 @@ Section language. Lemma eq_interp_flat_type_eta {var t T f} x : @interp_flat_type_eta base_type_code var t T f x = f x. - Proof. t. Qed. + Proof using Type. t. Qed. (* Local *) Hint Rewrite @eq_interp_flat_type_eta. Lemma eq_interp_flat_type_eta' {var t T f} x : @interp_flat_type_eta' base_type_code var t T f x = f x. - Proof. t. Qed. + Proof using Type. t. Qed. (* Local *) Hint Rewrite @eq_interp_flat_type_eta'. Lemma interpf_exprf_eta {t e} : interpf (@interp_op) (exprf_eta (t:=t) e) = interpf (@interp_op) e. - Proof. t. Qed. + Proof using Type. t. Qed. (* Local *) Hint Rewrite @interpf_exprf_eta. Lemma interpf_exprf_eta' {t e} : interpf (@interp_op) (exprf_eta' (t:=t) e) = interpf (@interp_op) e. - Proof. t. Qed. + Proof using Type. t. Qed. (* Local *) Hint Rewrite @interpf_exprf_eta'. Lemma interp_expr_eta {t e} : forall x, interp (@interp_op) (expr_eta (t:=t) e) x = interp (@interp_op) e x. - Proof. t. Qed. + Proof using Type. t. Qed. Lemma interp_expr_eta' {t e} : forall x, interp (@interp_op) (expr_eta' (t:=t) e) x = interp (@interp_op) e x. - Proof. t. Qed. + Proof using Type. t. Qed. Lemma InterpExprEta {t e} : forall x, Interp (@interp_op) (ExprEta (t:=t) e) x = Interp (@interp_op) e x. - Proof. apply interp_expr_eta. Qed. + Proof using Type. apply interp_expr_eta. Qed. Lemma InterpExprEta' {t e} : forall x, Interp (@interp_op) (ExprEta' (t:=t) e) x = Interp (@interp_op) e x. - Proof. apply interp_expr_eta'. Qed. + Proof using Type. apply interp_expr_eta'. Qed. Lemma InterpExprEta_arrow {s d e} : forall x, Interp (t:=Arrow s d) (@interp_op) (ExprEta (t:=Arrow s d) e) x = Interp (@interp_op) e x. - Proof. exact (@InterpExprEta (Arrow s d) e). Qed. + Proof using Type. exact (@InterpExprEta (Arrow s d) e). Qed. Lemma InterpExprEta'_arrow {s d e} : forall x, Interp (t:=Arrow s d) (@interp_op) (ExprEta' (t:=Arrow s d) e) x = Interp (@interp_op) e x. - Proof. exact (@InterpExprEta' (Arrow s d) e). Qed. + Proof using Type. exact (@InterpExprEta' (Arrow s d) e). Qed. Lemma eq_interp_eta {t e} : forall x, interp_eta interp_op (t:=t) e x = interp interp_op e x. - Proof. apply eq_interp_flat_type_eta. Qed. + Proof using Type. apply eq_interp_flat_type_eta. Qed. Lemma eq_InterpEta {t e} : forall x, InterpEta interp_op (t:=t) e x = Interp interp_op e x. - Proof. apply eq_interp_eta. Qed. + Proof using Type. apply eq_interp_eta. Qed. End language. Hint Rewrite @eq_interp_flat_type_eta @eq_interp_flat_type_eta' @interpf_exprf_eta @interpf_exprf_eta' @interp_expr_eta @interp_expr_eta' @InterpExprEta @InterpExprEta' @InterpExprEta_arrow @InterpExprEta'_arrow @eq_interp_eta @eq_InterpEta : reflective_interp. diff --git a/src/Reflection/EtaWf.v b/src/Reflection/EtaWf.v index abfef410b..240f5a1e3 100644 --- a/src/Reflection/EtaWf.v +++ b/src/Reflection/EtaWf.v @@ -53,13 +53,13 @@ Section language. : wf (expr_eta_gen eta exprf_eta1 (t:=t) e1) (expr_eta_gen eta exprf_eta2 (t:=t) e2) <-> wf e1 e2. - Proof. unfold expr_eta_gen; t; inversion_wf_step; t. Qed. + Proof using Type*. unfold expr_eta_gen; t; inversion_wf_step; t. Qed. End gen_type. Lemma wff_exprf_eta_gen {t e1 e2} G : wff G (exprf_eta_gen eta (t:=t) e1) (exprf_eta_gen eta (t:=t) e2) <-> @wff base_type_code op var1 var2 G t e1 e2. - Proof. + Proof using eq_eta. revert G; induction e1; first [ progress invert_expr | destruct e2 ]; t; inversion_wf_step; t. Qed. @@ -71,22 +71,22 @@ Section language. Lemma wff_exprf_eta {G t e1 e2} : wff G (exprf_eta (t:=t) e1) (exprf_eta (t:=t) e2) <-> @wff base_type_code op var1 var2 G t e1 e2. - Proof. setoid_rewrite wff_exprf_eta_gen; reflexivity. Qed. + Proof using Type. setoid_rewrite wff_exprf_eta_gen; reflexivity. Qed. Lemma wff_exprf_eta' {G t e1 e2} : wff G (exprf_eta' (t:=t) e1) (exprf_eta' (t:=t) e2) <-> @wff base_type_code op var1 var2 G t e1 e2. - Proof. setoid_rewrite wff_exprf_eta_gen; intuition. Qed. + Proof using Type. setoid_rewrite wff_exprf_eta_gen; intuition. Qed. Lemma wf_expr_eta {t e1 e2} : wf (expr_eta (t:=t) e1) (expr_eta (t:=t) e2) <-> @wf base_type_code op var1 var2 t e1 e2. - Proof. + Proof using Type. unfold expr_eta, exprf_eta. setoid_rewrite wf_expr_eta_gen; intuition (solve [ eapply wff_exprf_eta_gen; [ | eassumption ]; intuition ] || eauto). Qed. Lemma wf_expr_eta' {t e1 e2} : wf (expr_eta' (t:=t) e1) (expr_eta' (t:=t) e2) <-> @wf base_type_code op var1 var2 t e1 e2. - Proof. + Proof using Type. unfold expr_eta', exprf_eta'. setoid_rewrite wf_expr_eta_gen; intuition (solve [ eapply wff_exprf_eta_gen; [ | eassumption ]; intuition ] || eauto). Qed. @@ -97,7 +97,7 @@ Section language. (eq_eta : forall A B x, @eta A B x = x) {t e} : Wf (ExprEtaGen (@eta) e) <-> @Wf base_type_code op t e. - Proof. + Proof using Type. split; intros H var1 var2; specialize (H var1 var2); revert H; eapply wf_expr_eta_gen; try eassumption; intros; symmetry; apply wff_exprf_eta_gen; @@ -106,13 +106,13 @@ Section language. Lemma Wf_ExprEta_iff {t e} : Wf (ExprEta e) <-> @Wf base_type_code op t e. - Proof. + Proof using Type. unfold Wf; setoid_rewrite wf_expr_eta; reflexivity. Qed. Lemma Wf_ExprEta'_iff {t e} : Wf (ExprEta' e) <-> @Wf base_type_code op t e. - Proof. + Proof using Type. unfold Wf; setoid_rewrite wf_expr_eta'; reflexivity. Qed. Definition Wf_ExprEta {t e} : Wf e -> Wf (ExprEta e) := proj2 (@Wf_ExprEta_iff t e). diff --git a/src/Reflection/ExprInversion.v b/src/Reflection/ExprInversion.v index 450824f2f..645555cb5 100644 --- a/src/Reflection/ExprInversion.v +++ b/src/Reflection/ExprInversion.v @@ -147,7 +147,7 @@ Section language. Lemma interpf_invert_Abs interp_op {T e} x : Syntax.interpf interp_op (@invert_Abs interp_base_type T e x) = Syntax.interp interp_op e x. - Proof. destruct e; reflexivity. Qed. + Proof using Type. destruct e; reflexivity. Qed. End language. Global Arguments invert_Var {_ _ _ _} _. diff --git a/src/Reflection/InlineCastInterp.v b/src/Reflection/InlineCastInterp.v index aa9fbb119..f885fbd16 100644 --- a/src/Reflection/InlineCastInterp.v +++ b/src/Reflection/InlineCastInterp.v @@ -46,11 +46,11 @@ Section language. Lemma cast_val_id A (v : exprf _ _ (Tbase A)) : cast_val A A (interpf interp_op v) = interpf interp_op v. - Proof. rewrite <- !interpf_cast, !interpf_Cast_id; reflexivity. Qed. + Proof using interpf_Cast_id interpf_cast. rewrite <- !interpf_cast, !interpf_Cast_id; reflexivity. Qed. Lemma interpf_squash_cast a b c e1 : interpf interp_op (@squash_cast _ a b c e1) = interpf interp_op (Cast _ b c (Cast _ a b e1)). - Proof. + Proof using cast_val_squash interpf_Cast_id interpf_cast. unfold squash_cast; repeat first [ progress break_innermost_match | intro @@ -67,7 +67,7 @@ Section language. Lemma interpf_maybe_push_cast t e e' : @maybe_push_cast _ t e = Some e' -> interpf interp_op e' = interpf interp_op e. - Proof. + Proof using cast_val_squash interpf_Cast_id interpf_cast is_cast_correct. revert e'; induction e; repeat first [ reflexivity | discriminate @@ -97,7 +97,7 @@ Section language. Lemma interpf_exprf_of_push_cast t e : interpf interp_op (exprf_of_inline_directive (@push_cast _ t e)) = interpf interp_op e. - Proof. + Proof using cast_val_squash interpf_Cast_id interpf_cast is_cast_correct. unfold push_cast; break_innermost_match; simpl; try reflexivity. match goal with H : _ |- _ => apply interpf_maybe_push_cast in H end. assumption. @@ -109,7 +109,7 @@ Section language. : forall x, Interp interp_op (@InlineCast t e) x = Interp interp_op e x. - Proof. apply InterpInlineConstGen; auto. Qed. + Proof using cast_val_squash interpf_Cast_id interpf_cast is_cast_correct. apply InterpInlineConstGen; auto. Qed. End language. Hint Rewrite @interpf_exprf_of_push_cast @InterpInlineCast using solve [ eassumption | eauto with wf ] : reflective_interp. diff --git a/src/Reflection/InlineCastWf.v b/src/Reflection/InlineCastWf.v index c973335d0..a61455c4f 100644 --- a/src/Reflection/InlineCastWf.v +++ b/src/Reflection/InlineCastWf.v @@ -38,7 +38,7 @@ Section language. Lemma wff_squash_cast var1 var2 a b c e1 e2 G (Hwf : wff G e1 e2) : wff G (@squash_cast var1 a b c e1) (@squash_cast var2 a b c e2). - Proof. + Proof using wff_Cast. unfold squash_cast; break_innermost_match; auto with wf. Qed. @@ -51,7 +51,7 @@ Section language. | None, None => True | Some _, None | None, Some _ => False end. - Proof. + Proof using wff_Cast. induction Hwf; repeat match goal with | [ |- wff _ (squash_cast _ _ _ _) (squash_cast _ _ _ _) ] @@ -81,7 +81,7 @@ Section language. : @maybe_push_cast var1 t e1 = Some e1' -> @maybe_push_cast var2 t e2 = Some e2' -> wff G e1' e2'. - Proof. + Proof using wff_Cast. intros H0 H1; eapply wff_maybe_push_cast_match in Hwf. rewrite H0, H1 in Hwf; assumption. Qed. @@ -103,7 +103,7 @@ Section language. Lemma wff_push_cast var1 var2 t e1 e2 G (Hwf : wff G e1 e2) : wff_inline_directive G (@push_cast var1 t e1) (@push_cast var2 t e2). - Proof. + Proof using wff_Cast. pose proof (wff_maybe_push_cast_match Hwf). unfold push_cast; destruct t; break_innermost_match; @@ -119,13 +119,13 @@ Section language. : wff G (exprf_of_inline_directive (@push_cast var1 t e1)) (exprf_of_inline_directive (@push_cast var2 t e2)). - Proof. apply wff_push_cast; assumption. Qed. + Proof using wff_Cast. apply wff_push_cast; assumption. Qed. Local Hint Resolve wff_push_cast. Lemma Wf_InlineCast {t} e (Hwf : Wf e) : Wf (@InlineCast t e). - Proof. apply Wf_InlineConstGen; auto. Qed. + Proof using wff_Cast. apply Wf_InlineConstGen; auto. Qed. End language. Hint Resolve Wf_InlineCast : wf. diff --git a/src/Reflection/InlineInterp.v b/src/Reflection/InlineInterp.v index 7bee4a70c..cb9276d9a 100644 --- a/src/Reflection/InlineInterp.v +++ b/src/Reflection/InlineInterp.v @@ -73,14 +73,14 @@ Section language. (x, x')) G -> interpf interp_op x = x') : interpf interp_op (inline_const_genf postprocess e1) = interpf interp_op e2. - Proof. + Proof using Type. clear -wf H Hpostprocess. induction wf; t_fin. Qed. Lemma interpf_postprocess_for_const is_const t e : interpf interp_op (exprf_of_inline_directive (postprocess_for_const is_const t e)) = interpf interp_op e. - Proof. + Proof using Type. unfold postprocess_for_const; t_fin. Qed. @@ -94,7 +94,7 @@ Section language. (x, x')) G -> interpf interp_op x = x') : interpf interp_op (inline_constf is_const e1) = interpf interp_op e2. - Proof. eapply interpf_inline_const_genf; eauto. Qed. + Proof using Type. eapply interpf_inline_const_genf; eauto. Qed. Local Hint Resolve interpf_inline_constf. @@ -102,7 +102,7 @@ Section language. (wf : @wf _ _ t e1 e2) (Hpostprocess : forall t e, interpf interp_op (exprf_of_inline_directive (postprocess t e)) = interpf interp_op e) : forall x, interp interp_op (inline_const_gen postprocess e1) x = interp interp_op e2 x. - Proof. + Proof using Type. destruct wf. simpl in *; intro; eapply (interpf_inline_const_genf postprocess); eauto. Qed. @@ -112,7 +112,7 @@ Section language. Lemma interp_inline_const is_const {t} e1 e2 (wf : @wf _ _ t e1 e2) : forall x, interp interp_op (inline_const is_const e1) x = interp interp_op e2 x. - Proof. + Proof using Type. eapply interp_inline_const_gen; eauto. Qed. @@ -120,7 +120,7 @@ Section language. (wf : Wf e) (Hpostprocess : forall t e, interpf interp_op (exprf_of_inline_directive (postprocess _ t e)) = interpf interp_op e) : forall x, Interp interp_op (InlineConstGen postprocess e) x = Interp interp_op e x. - Proof. + Proof using Type. unfold Interp, InlineConst. eapply (interp_inline_const_gen (postprocess _)); simpl; intuition. Qed. @@ -128,7 +128,7 @@ Section language. Lemma InterpInlineConst is_const {t} (e : Expr t) (wf : Wf e) : forall x, Interp interp_op (InlineConst is_const e) x = Interp interp_op e x. - Proof. + Proof using Type. eapply InterpInlineConstGen; eauto. Qed. End language. diff --git a/src/Reflection/InlineWf.v b/src/Reflection/InlineWf.v index 084f0d46b..20ae25010 100644 --- a/src/Reflection/InlineWf.v +++ b/src/Reflection/InlineWf.v @@ -86,7 +86,7 @@ Section language. wff G e1 e2 -> wff_inline_directive G (postprocess1 t e1) (postprocess2 t e2)) : @wff var1 var2 G t (inline_const_genf postprocess1 e1) (inline_const_genf postprocess2 e2). - Proof. + Proof using Type. revert dependent G; induction wf; simpl in *; auto; intros; []. repeat match goal with | [ H : context[List.In _ (_ ++ _)] |- _ ] @@ -156,7 +156,7 @@ Section language. (e2 : @exprf var2 t) (Hwf : wff G e1 e2) : wff_inline_directive G (postprocess_for_const is_const t e1) (postprocess_for_const is_const t e2). - Proof. + Proof using Type. destruct e1; unfold postprocess_for_const; repeat first [ progress subst | intro @@ -182,7 +182,7 @@ Section language. -> wff G x x') (wf : wff G' e1 e2) : @wff var1 var2 G t (inline_constf is_const e1) (inline_constf is_const e2). - Proof. eapply wff_inline_const_genf; eauto. Qed. + Proof using Type. eapply wff_inline_const_genf; eauto. Qed. Lemma wf_inline_const_gen postprocess1 postprocess2 {t} e1 e2 (Hwf : wf e1 e2) @@ -190,7 +190,7 @@ Section language. wff G e1 e2 -> wff_inline_directive G (postprocess1 t e1) (postprocess2 t e2)) : @wf var1 var2 t (inline_const_gen postprocess1 e1) (inline_const_gen postprocess2 e2). - Proof. + Proof using Type. destruct Hwf; constructor; intros. eapply wff_inline_const_genf; eauto using wff_SmartVarVarf_nil. Qed. @@ -198,7 +198,7 @@ Section language. Lemma wf_inline_const is_const {t} e1 e2 (Hwf : wf e1 e2) : @wf var1 var2 t (inline_const is_const e1) (inline_const is_const e2). - Proof. eapply wf_inline_const_gen; eauto. Qed. + Proof using Type. eapply wf_inline_const_gen; eauto. Qed. End with_var. Lemma Wf_InlineConstGen postprocess {t} (e : Expr t) @@ -207,7 +207,7 @@ Section language. wff G e1 e2 -> wff_inline_directive G (postprocess var1 t e1) (postprocess var2 t e2)) : Wf (InlineConstGen postprocess e). - Proof. + Proof using Type. intros var1 var2. apply (@wf_inline_const_gen var1 var2 (postprocess _) (postprocess _) t (e _) (e _)); simpl; auto. Qed. @@ -215,7 +215,7 @@ Section language. Lemma Wf_InlineConst is_const {t} (e : Expr t) (Hwf : Wf e) : Wf (InlineConst is_const e). - Proof. + Proof using Type. intros var1 var2. apply (@wf_inline_const var1 var2 is_const t (e _) (e _)); simpl. apply Hwf. diff --git a/src/Reflection/InputSyntax.v b/src/Reflection/InputSyntax.v index 832f5fdfd..123e4f851 100644 --- a/src/Reflection/InputSyntax.v +++ b/src/Reflection/InputSyntax.v @@ -147,13 +147,13 @@ Section language. Lemma SmartConst_correct t v : Syntax.interpf interp_op (SmartConst make_const t v) = v. - Proof. + Proof using Type*. induction t; try destruct v; simpl in *; congruence. Qed. Lemma compilef_correct {t} (e : @exprf interp_flat_type t) : Syntax.interpf interp_op (compilef make_const e) = interpf interp_op e. - Proof. + Proof using Type*. induction e; repeat match goal with | _ => reflexivity @@ -170,7 +170,7 @@ Section language. Lemma compile_flat_correct {T} (e : expr (Tflat T)) : forall x, Syntax.interp interp_op (compile make_const e) x = interp interp_op e. - Proof. + Proof using Type*. intros []; simpl. let G := match goal with |- ?G => G end in let G := match (eval pattern T, e in G) with ?G _ _ => G end in @@ -187,11 +187,11 @@ Section language. Lemma Compile_flat_correct_flat {T} (e : Expr (Tflat T)) : forall x, Syntax.Interp interp_op (Compile make_const e) x = Interp interp_op e. - Proof. apply compile_flat_correct. Qed. + Proof using Type*. apply compile_flat_correct. Qed. Lemma Compile_correct {src dst} (e : @Expr (Arrow src (Tflat dst))) : forall x, Syntax.Interp interp_op (Compile make_const e) x = Interp interp_op e x. - Proof. + Proof using Type*. unfold Interp, Compile, Syntax.Interp; simpl. pose (e interp_flat_type) as E. repeat match goal with |- context[e ?f] => change (e f) with E end. diff --git a/src/Reflection/InterpByIsoProofs.v b/src/Reflection/InterpByIsoProofs.v index 2612a1c79..07ad8ed62 100644 --- a/src/Reflection/InterpByIsoProofs.v +++ b/src/Reflection/InterpByIsoProofs.v @@ -23,13 +23,13 @@ Section language. Lemma interpf_retr_id {t} (e : @exprf interp_base_type t) : interpf_retr (fun _ x => x) (fun _ x => x) e = interpf interp_op e. - Proof. + Proof using Type. induction e; simpl; cbv [LetIn.Let_In]; rewrite_hyp ?*; rewrite ?SmartVarfMap_id; reflexivity. Qed. Lemma interp_retr_id {t} (e : @expr interp_base_type t) : forall x, interp_retr (fun _ x => x) (fun _ x => x) e x = interp interp_op e x. - Proof. + Proof using Type. destruct e; simpl; intros; rewrite interpf_retr_id, SmartVarfMap_id; reflexivity. Qed. @@ -49,7 +49,7 @@ Section language. (SmartVarfMap (t:=t1) var1_of_interp e1) (SmartVarfMap var2_of_interp e1))) : interp_of_var1 t x1 = interp_of_var2 t x2. - Proof. + Proof using interp_of_var12. repeat first [ progress repeat autorewrite with core in * | progress subst | progress inversion_sigma @@ -75,7 +75,7 @@ Section language. (Hwf : wff G e1 e2) : interpf_retr var1_of_interp interp_of_var1 e1 = interpf_retr var2_of_interp interp_of_var2 e2. - Proof. + Proof using interp_of_var12. induction Hwf; simpl; rewrite_hyp ?*; try reflexivity; auto. { match goal with H : _ |- _ => apply H end. intros ???; rewrite List.in_app_iff. @@ -86,7 +86,7 @@ Section language. : forall x, interp_retr var1_of_interp interp_of_var1 e1 x = interp_retr var2_of_interp interp_of_var2 e2 x. - Proof. + Proof using interp_of_var12. destruct Hwf; simpl; repeat intro; subst; eapply wff_interpf_retr; eauto. Qed. End with_var2. @@ -102,7 +102,7 @@ Section language. -> interp_of_var t x1 = x2) (Hwf : wff G e1 e2) : interpf_retr var_of_interp interp_of_var e1 = interpf interp_op e2. - Proof. + Proof using var_is_retract. erewrite wff_interpf_retr, interpf_retr_id; eauto. Qed. Lemma wf_interp_retr_correct {t} (e1 : @expr var t) (e2 : @expr interp_base_type t) @@ -110,7 +110,7 @@ Section language. x : interp_retr var_of_interp interp_of_var e1 x = interp interp_op e2 x. - Proof. + Proof using var_is_retract. erewrite wf_interp_retr, interp_retr_id; eauto. Qed. End with_var. diff --git a/src/Reflection/InterpProofs.v b/src/Reflection/InterpProofs.v index 88ceaac56..5d8322441 100644 --- a/src/Reflection/InterpProofs.v +++ b/src/Reflection/InterpProofs.v @@ -22,11 +22,11 @@ Section language. : Syntax.interpf interp_op (LetIn (tx:=tx) ex (tC:=tC) eC) = dlet x := Syntax.interpf interp_op ex in Syntax.interpf interp_op (eC x). - Proof. reflexivity. Qed. + Proof using Type. reflexivity. Qed. Lemma interpf_SmartVarf t v : Syntax.interpf interp_op (SmartVarf (t:=t) v) = v. - Proof. + Proof using Type. unfold SmartVarf; induction t; repeat match goal with | _ => reflexivity @@ -42,7 +42,7 @@ Section language. t (x, x')) (flatten_binding_list (t := t') (SmartVarVarf v) v)) : interpf interp_op x = x'. - Proof. + Proof using Type. clear -Hin. induction t'; simpl in *; try tauto. { intuition (inversion_sigma; inversion_prod; subst; eauto). } @@ -57,7 +57,7 @@ Section language. t (x, x')) (flatten_binding_list (t := t') (SmartVarVarf v') v)) : interpf interp_op x = x'. - Proof. + Proof using Type. subst; eapply interpf_SmartVarVarf; eassumption. Qed. End language. diff --git a/src/Reflection/InterpWf.v b/src/Reflection/InterpWf.v index e4c3e7de0..5f76e0791 100644 --- a/src/Reflection/InterpWf.v +++ b/src/Reflection/InterpWf.v @@ -30,7 +30,7 @@ Section language. (HIn : List.In (existT (fun t : base_type_code => (interp_base_type t * interp_base_type t)%type) t (x, x')%core) (flatten_binding_list (t:=T) e e)) : x = x'. - Proof. + Proof using Type. induction T; simpl in *; [ | | rewrite List.in_app_iff in HIn ]; repeat first [ progress destruct_head or | progress destruct_head False @@ -53,7 +53,7 @@ Section language. -> x = x') (Rwf : wff G e1 e2) : interpf e1 = interpf e2. - Proof. + Proof using Type. induction Rwf; simpl; auto; specialize_by auto; try congruence. rewrite_hyp !*; auto. @@ -73,7 +73,7 @@ Section language. {t} {e1 e2 : expr t} (Rwf : wf e1 e2) : forall x, interp e1 x = interp e2 x. - Proof. + Proof using Type. destruct Rwf; simpl; eauto. Qed. End wf. diff --git a/src/Reflection/InterpWfRel.v b/src/Reflection/InterpWfRel.v index b827c235a..40288232a 100644 --- a/src/Reflection/InterpWfRel.v +++ b/src/Reflection/InterpWfRel.v @@ -39,7 +39,7 @@ Section language. (HIn : List.In (existT (fun t : base_type_code => (interp_base_type1 t * interp_base_type2 t)%type) t (x, x')%core) (flatten_binding_list (t:=T) e1 e2)) : R t x x'. - Proof. + Proof using Type. induction T; simpl in *; try tauto; [ | rewrite List.in_app_iff in HIn ]; repeat first [ progress destruct_head or | progress destruct_head False @@ -61,7 +61,7 @@ Section language. -> R t x x') (Rwf : wff G e1 e2) : interp_flat_type_rel_pointwise R (interpf1 e1) (interpf2 e2). - Proof. + Proof using Type*. induction Rwf; simpl; auto. repeat match goal with | [ H : context[List.In _ (_ ++ _)] |- _ ] @@ -79,7 +79,7 @@ Section language. {t} {e1 : expr1 t} {e2 : expr2 t} (Rwf : wf e1 e2) : interp_type_rel_pointwise R (interp1 e1) (interp2 e2). - Proof. + Proof using Type*. destruct Rwf; simpl; repeat intro; eauto. Qed. @@ -87,7 +87,7 @@ Section language. {t} {e : Expr t} (Rwf : Wf e) : interp_type_rel_pointwise R (Interp1 e) (Interp2 e). - Proof. + Proof using Type*. unfold Interp, Wf in *; apply interp_wf; simpl; intuition. Qed. End wf. diff --git a/src/Reflection/LinearizeInterp.v b/src/Reflection/LinearizeInterp.v index e6acac0d6..293d80a34 100644 --- a/src/Reflection/LinearizeInterp.v +++ b/src/Reflection/LinearizeInterp.v @@ -53,14 +53,14 @@ Section language. Lemma interpf_under_letsf {t tC} (ex : exprf t) (eC : _ -> exprf tC) : interpf interp_op (under_letsf ex eC) = let x := interpf interp_op ex in interpf interp_op (eC x). - Proof. + Proof using Type. clear. induction ex; t_fin. Qed. Lemma interpf_linearizef {t} e : interpf interp_op (linearizef (t:=t) e) = interpf interp_op e. - Proof. + Proof using Type. clear. induction e; repeat first [ progress rewrite ?interpf_under_letsf, ?interpf_SmartVarf @@ -72,13 +72,13 @@ Section language. Lemma interp_linearize {t} e : forall x, interp interp_op (linearize (t:=t) e) x = interp interp_op e x. - Proof. + Proof using Type. induction e; simpl; eauto. Qed. Lemma InterpLinearize {t} (e : Expr t) : forall x, Interp interp_op (Linearize e) x = Interp interp_op e x. - Proof. + Proof using Type. unfold Interp, Linearize. eapply interp_linearize. Qed. diff --git a/src/Reflection/LinearizeWf.v b/src/Reflection/LinearizeWf.v index 4e4b4fc38..b12e83b56 100644 --- a/src/Reflection/LinearizeWf.v +++ b/src/Reflection/LinearizeWf.v @@ -102,7 +102,7 @@ Section language. wff (flatten_binding_list x1 x2 ++ G) (eC1 x1) (eC2 x2)) {struct e1} : @wff var1 var2 G tC (under_letsf e1 eC1) (under_letsf e2 eC2). - Proof. + Proof using Type. revert H. set (e1v := e1) in *. destruct e1 as [ | | ? ? ? args | tx ex tC0 eC0 | ? ex ? ey ]; @@ -153,7 +153,7 @@ Section language. Lemma wff_linearizef G {t} e1 e2 : @wff var1 var2 G t e1 e2 -> @wff var1 var2 G t (linearizef e1) (linearizef e2). - Proof. + Proof using Type. induction 1; t_fin ltac:(apply wff_under_letsf). Qed. @@ -162,13 +162,13 @@ Section language. Lemma wf_linearize {t} e1 e2 : @wf var1 var2 t e1 e2 -> @wf var1 var2 t (linearize e1) (linearize e2). - Proof. + Proof using Type. destruct 1; constructor; auto. Qed. End with_var. Lemma Wf_Linearize {t} (e : Expr t) : Wf e -> Wf (Linearize e). - Proof. + Proof using Type. intros wf var1 var2; apply wf_linearize, wf. Qed. End language. diff --git a/src/Reflection/MapCastByDeBruijnInterp.v b/src/Reflection/MapCastByDeBruijnInterp.v index 74622223e..90cbad00c 100644 --- a/src/Reflection/MapCastByDeBruijnInterp.v +++ b/src/Reflection/MapCastByDeBruijnInterp.v @@ -78,7 +78,7 @@ Section language. Interp interp_op_bounds e input_bounds = b /\ @inbounds _ b (Interp interp_op e v) /\ cast_back _ _ (Interp interp_op e' v') = (Interp interp_op e v). - Proof. + Proof using base_type_code_lb interp_op_bounds_correct pull_cast_back. unfold MapCastByDeBruijn.MapCast, MapCastCompile, MapCastDoCast, MapCastDoInterp, option_map; intros b e'. break_innermost_match; try congruence; intros ? v v'. inversion_option; inversion_sigma; subst; simpl in *; intros. diff --git a/src/Reflection/MapCastByDeBruijnWf.v b/src/Reflection/MapCastByDeBruijnWf.v index fd8b824ca..4fd3975f7 100644 --- a/src/Reflection/MapCastByDeBruijnWf.v +++ b/src/Reflection/MapCastByDeBruijnWf.v @@ -72,7 +72,7 @@ Section language. (input_bounds : interp_flat_type interp_base_type_bounds (domain t)) : forall {b} e' (He':MapCast e input_bounds = Some (existT _ b e')) (Hwf : Wf e), Wf e'. - Proof. + Proof using base_type_code_lb. unfold MapCastByDeBruijn.MapCast, MapCastCompile, MapCastDoCast, MapCastDoInterp, option_map; intros b e'. break_innermost_match; try congruence; intros ? v v'. inversion_option; inversion_sigma; subst; simpl in *; intros. @@ -100,7 +100,7 @@ Section language. (He':MapCast e input_bounds = Some (existT _ b e')) (Hwf : Wf e), Wf e'. - Proof. exact (@Wf_MapCast (Arrow s d) e input_bounds). Qed. + Proof using base_type_code_lb. exact (@Wf_MapCast (Arrow s d) e input_bounds). Qed. End language. Hint Resolve Wf_MapCast Wf_MapCast_arrow : wf. diff --git a/src/Reflection/MapCastInterp.v b/src/Reflection/MapCastInterp.v index e3f93af86..528e69e12 100644 --- a/src/Reflection/MapCastInterp.v +++ b/src/Reflection/MapCastInterp.v @@ -64,7 +64,7 @@ Section language. R t x : is_true (@bounds_are_recursively_goodb R t x) <-> @bounds_are_recursively_good (fun t x => is_true (R t x)) t x. - Proof. + Proof using Type. unfold is_true. clear; induction x; simpl in *; rewrite ?Bool.andb_true_iff; try setoid_rewrite interp_flat_type_rel_pointwise1_gen_Prop_iff_bool; @@ -81,7 +81,7 @@ Section language. := (@interp_flat_type_rel_pointwise1 _ _ bound_is_good). Lemma bounds_are_good_when_recursively_good {t} e : @bounds_are_recursively_good bound_is_good t e -> bounds_are_good (interpf interp_op2 e). - Proof. + Proof using Type. induction e; simpl; unfold LetIn.Let_In; intuition auto. Qed. Local Hint Resolve bounds_are_good_when_recursively_good. @@ -227,7 +227,7 @@ Section language. = interpf interp_op1 e1 /\ R (interpf interp_op1 (@mapf_interp_cast interp_base_type1 t1 e1 t1 ebounds)) (interpf interp_op2 ebounds). - Proof. induction Hwf; repeat t_step. Qed. + Proof using R_transfer_op interpf_transfer_op. induction Hwf; repeat t_step. Qed. Local Hint Resolve interpf_mapf_interp_cast_and_rel. @@ -239,7 +239,7 @@ Section language. (Hwf : wff G e1 ebounds) : interpf interp_op1 (@mapf_interp_cast interp_base_type1 t1 e1 t1 ebounds) = interpf interp_op1 e1. - Proof. eapply interpf_mapf_interp_cast_and_rel; eassumption. Qed. + Proof using R_transfer_op interpf_transfer_op. eapply interpf_mapf_interp_cast_and_rel; eassumption. Qed. Lemma interp_map_interp_cast_and_rel {t1} e1 ebounds @@ -252,7 +252,7 @@ Section language. = interp interp_op1 e1 x /\ R (interp interp_op1 (@map_interp_cast interp_base_type1 t1 e1 t1 ebounds args2) x) (interp interp_op2 ebounds args2). - Proof. destruct Hwf; intros; eapply interpf_mapf_interp_cast_and_rel; eauto. Qed. + Proof using R_transfer_op interpf_transfer_op. destruct Hwf; intros; eapply interpf_mapf_interp_cast_and_rel; eauto. Qed. Lemma interp_map_interp_cast {t1} e1 ebounds @@ -263,7 +263,7 @@ Section language. R x args2 -> interp interp_op1 (@map_interp_cast interp_base_type1 t1 e1 t1 ebounds args2) x = interp interp_op1 e1 x. - Proof. intros; eapply interp_map_interp_cast_and_rel; eassumption. Qed. + Proof using R_transfer_op interpf_transfer_op. intros; eapply interp_map_interp_cast_and_rel; eassumption. Qed. Lemma InterpMapInterpCastAndRel {t} e @@ -276,7 +276,7 @@ Section language. = Interp interp_op1 e x /\ R (Interp interp_op1 (@MapInterpCast t e args) x) (Interp interp_op2 e args). - Proof. apply interp_map_interp_cast_and_rel; auto. Qed. + Proof using R_transfer_op interpf_transfer_op. apply interp_map_interp_cast_and_rel; auto. Qed. Lemma InterpMapInterpCast {t} e @@ -287,5 +287,5 @@ Section language. R x args -> Interp interp_op1 (@MapInterpCast t e args) x = Interp interp_op1 e x. - Proof. apply interp_map_interp_cast; auto. Qed. + Proof using R_transfer_op interpf_transfer_op. apply interp_map_interp_cast; auto. Qed. End language. diff --git a/src/Reflection/MapCastWf.v b/src/Reflection/MapCastWf.v index 717f8de60..54e8d0020 100644 --- a/src/Reflection/MapCastWf.v +++ b/src/Reflection/MapCastWf.v @@ -102,7 +102,7 @@ Section language. : wff G1 (@mapf_interp_cast ovar1 t1 e1 t1 ebounds) (@mapf_interp_cast ovar2 t1 e2 t1 ebounds). - Proof. + Proof using wff_transfer_op. revert dependent Gbounds; revert ebounds; induction Hwf; repeat match goal with @@ -130,7 +130,7 @@ Section language. (Hwf : wf e1 e2) : wf (@map_interp_cast ovar1 t1 e1 t1 ebounds args2) (@map_interp_cast ovar2 t1 e2 t1 ebounds args2). - Proof. + Proof using wff_transfer_op. destruct Hwf; repeat match goal with | _ => solve [ constructor; eauto @@ -163,7 +163,7 @@ Section language. args (Hwf : Wf e) : Wf (@MapInterpCast t e args). - Proof. + Proof using wff_transfer_op. intros ??; apply wf_map_interp_cast; auto. Qed. End gen. diff --git a/src/Reflection/Named/CompileInterp.v b/src/Reflection/Named/CompileInterp.v index 6cb075f08..100d53aa3 100644 --- a/src/Reflection/Named/CompileInterp.v +++ b/src/Reflection/Named/CompileInterp.v @@ -54,7 +54,7 @@ Section language. (HGls : forall t n x, List.In (existT _ t (n, x)%core) G -> List.In (Some n) ls -> False) : Named.interpf (interp_op:=interp_op) (ctx:=ctx) v = Some (interpf interp_op e'). - Proof. + Proof using ContextOk Name_dec base_type_dec. revert dependent ctx; revert dependent ls; induction Hwf; repeat first [ progress intros | progress subst @@ -135,7 +135,7 @@ Section language. (H : ocompile e ls = Some f) : forall v, Named.interp (interp_op:=interp_op) (ctx:=ctx) f v = Some (interp interp_op e' v). - Proof. + Proof using ContextOk Name_dec base_type_dec. revert H; destruct Hwf; repeat first [ progress simpl in * | progress unfold option_map, Named.interp in * @@ -179,7 +179,7 @@ Section language. (HGls : forall t n x, List.In (existT _ t (n, x)%core) G -> List.In n ls -> False) : Named.interpf (interp_op:=interp_op) (ctx:=ctx) v = Some (interpf interp_op e'). - Proof. + Proof using ContextOk Name_dec base_type_dec. eapply interpf_ocompilef; try eassumption. setoid_rewrite List.in_map_iff; intros; destruct_head' ex; destruct_head' and; inversion_option; subst. eauto. @@ -192,5 +192,5 @@ Section language. (H : compile e ls = Some f) : forall v, Named.interp (interp_op:=interp_op) (ctx:=ctx) f v = Some (interp interp_op e' v). - Proof. eapply interp_ocompile; eassumption. Qed. + Proof using ContextOk Name_dec base_type_dec. eapply interp_ocompile; eassumption. Qed. End language. diff --git a/src/Reflection/Named/CompileWf.v b/src/Reflection/Named/CompileWf.v index 3f322aed5..5fb17b18d 100644 --- a/src/Reflection/Named/CompileWf.v +++ b/src/Reflection/Named/CompileWf.v @@ -55,7 +55,7 @@ Section language. (Hls : oname_list_unique ls) (HGls : forall t n x, List.In (existT _ t (n, x)%core) G -> List.In (Some n) ls -> False) : prop_of_option (nwff ctx v). - Proof. + Proof using ContextOk Name_dec base_type_dec. revert dependent ctx; revert dependent ls; induction Hwf; repeat first [ progress intros | progress subst @@ -165,7 +165,7 @@ Section language. (Hls : oname_list_unique ls) (H : ocompile e ls = Some f) : nwf ctx f. - Proof. + Proof using ContextOk Name_dec base_type_dec. revert H; destruct Hwf; repeat first [ progress simpl in * | progress unfold option_map, Named.interp in * @@ -210,7 +210,7 @@ Section language. (Hls : name_list_unique ls) (HGls : forall t n x, List.In (existT _ t (n, x)%core) G -> List.In n ls -> False) : prop_of_option (nwff ctx v). - Proof. + Proof using ContextOk Name_dec base_type_dec. eapply wff_ocompilef; try eassumption. setoid_rewrite List.in_map_iff; intros; destruct_head' ex; destruct_head' and; inversion_option; subst. eauto. @@ -222,5 +222,5 @@ Section language. (Hls : name_list_unique ls) (H : compile e ls = Some f) : nwf ctx f. - Proof. eapply wf_ocompile; eassumption. Qed. + Proof using ContextOk Name_dec base_type_dec. eapply wf_ocompile; eassumption. Qed. End language. diff --git a/src/Reflection/Named/ContextProperties.v b/src/Reflection/Named/ContextProperties.v index 4bd0325fb..c031d0af2 100644 --- a/src/Reflection/Named/ContextProperties.v +++ b/src/Reflection/Named/ContextProperties.v @@ -31,7 +31,7 @@ Section with_context. T N t n v : lookupb (extend ctx N (t:=T) v) n t = find_Name_and_val t n N v (lookupb ctx n t). - Proof. revert ctx; induction T; t. Qed. + Proof using ContextOk. revert ctx; induction T; t. Qed. Lemma find_Name_and_val_Some_None {var' var''} @@ -42,7 +42,7 @@ Section with_context. (H0 : @find_Name_and_val var' t n T N x default = Some v) (H1 : @find_Name_and_val var'' t n T N y default' = None) : default = Some v /\ default' = None. - Proof. + Proof using Type. revert dependent default; revert dependent default'; induction T; t. Qed. @@ -54,7 +54,7 @@ Section with_context. (H : @find_Name n T N <> None) : @find_Name_and_val var' t n T N x default = @find_Name_and_val var' t n T N x None. - Proof. revert default; induction T; t. Qed. + Proof using Type. revert default; induction T; t. Qed. Hint Rewrite @find_Name_and_val_default_to_None using congruence : ctx_db. Lemma find_Name_and_val_different @@ -64,7 +64,7 @@ Section with_context. {default} (H : @find_Name n T N = None) : @find_Name_and_val var' t n T N x default = default. - Proof. revert default; induction T; t. Qed. + Proof using Type. revert default; induction T; t. Qed. Hint Rewrite @find_Name_and_val_different using assumption : ctx_db. Lemma find_Name_and_val_wrong_type_iff @@ -75,7 +75,7 @@ Section with_context. (H : @find_Name n T N = Some t') : t <> t' <-> @find_Name_and_val var' t n T N x default = None. - Proof. split; revert default; induction T; t. Qed. + Proof using Type. split; revert default; induction T; t. Qed. Lemma find_Name_and_val_wrong_type {var'} {t t' n T N} @@ -84,14 +84,14 @@ Section with_context. (H : @find_Name n T N = Some t') (Ht : t <> t') : @find_Name_and_val var' t n T N x default = None. - Proof. eapply find_Name_and_val_wrong_type_iff; eassumption. Qed. + Proof using Type. eapply find_Name_and_val_wrong_type_iff; eassumption. Qed. Hint Rewrite @find_Name_and_val_wrong_type using congruence : ctx_db. Lemma find_Name_find_Name_and_val_wrong {var' n t' T V N} : find_Name n N = Some t' -> @find_Name_and_val var' t' n T N V None = None -> False. - Proof. induction T; t. Qed. + Proof using Type. induction T; t. Qed. Lemma find_Name_and_val_None_iff {var'} @@ -101,7 +101,7 @@ Section with_context. : (@find_Name n T N <> Some t /\ (@find_Name n T N <> None \/ default = None)) <-> @find_Name_and_val var' t n T N x default = None. - Proof. + Proof using Type. destruct (@find_Name n T N) eqn:?; unfold not; t; try solve [ eapply find_Name_and_val_wrong_type; [ eassumption | congruence ] | eapply find_Name_find_Name_and_val_wrong; eassumption @@ -117,14 +117,14 @@ Section with_context. else None | None => default end. - Proof. + Proof using Type. t; erewrite find_Name_and_val_wrong_type by solve [ eassumption | congruence ]; reflexivity. Qed. Lemma find_Name_and_val_find_Name_Some {var' t n T N V v} (H : @find_Name_and_val var' t n T N V None = Some v) : @find_Name n T N = Some t. - Proof. + Proof using Type. rewrite find_Name_and_val_split in H; break_match_hyps; subst; congruence. Qed. End with_context. diff --git a/src/Reflection/Named/ContextProperties/NameUtil.v b/src/Reflection/Named/ContextProperties/NameUtil.v index c494acd2d..4853f9a41 100644 --- a/src/Reflection/Named/ContextProperties/NameUtil.v +++ b/src/Reflection/Named/ContextProperties/NameUtil.v @@ -46,7 +46,7 @@ Section with_context. (H : split_onames _ ls = (Some N, ls')%core) : (exists t, @find_Name n T N = Some t) <-> List.In (Some n) (List.firstn (CountLets.count_pairs T) ls). - Proof. + Proof using Type. revert dependent ls; intro ls; revert ls ls'; induction T; intros; [ | | specialize (IHT1 (fst N) ls (snd (split_onames T1 ls))); specialize (IHT2 (snd N) (snd (split_onames T1 ls)) (snd (split_onames (T1 * T2) ls))) ]; @@ -71,7 +71,7 @@ Section with_context. (H : split_onames _ ls = (Some N, ls')%core) : (exists t, @find_Name n T N = Some t) <-> List.In (Some n) ls /\ ~List.In (Some n) ls'. - Proof. + Proof using Type. rewrite (split_onames_find_Name (ls':=ls') (ls:=ls)) by assumption. rewrite (surjective_pairing (split_onames _ _)) in H. rewrite fst_split_onames_firstn, snd_split_onames_skipn in H. @@ -86,7 +86,7 @@ Section with_context. (H : split_onames _ ls = (Some N, ls')%core) (Hfind : @find_Name n T N = Some t) : List.In (Some n) ls /\ ~List.In (Some n) ls'. - Proof. + Proof using Type. eapply split_onames_find_Name_Some_unique_iff; eauto. Qed. @@ -96,7 +96,7 @@ Section with_context. (H : split_onames _ ls = (Some N, ls')%core) : @find_Name_and_val var' t n T N V None = Some v <-> List.In (existT (fun t => (Name * var' t)%type) t (n, v)) (Wf.flatten_binding_list N V). - Proof. + Proof using Type. revert dependent ls; intro ls; revert ls ls'; induction T; intros; [ | | specialize (IHT1 (fst N) (fst V) ls (snd (split_onames T1 ls))); specialize (IHT2 (snd N) (snd V) (snd (split_onames T1 ls)) (snd (split_onames (T1 * T2) ls))) ]; diff --git a/src/Reflection/Named/ContextProperties/SmartMap.v b/src/Reflection/Named/ContextProperties/SmartMap.v index fd2144bed..89d0d1c5d 100644 --- a/src/Reflection/Named/ContextProperties/SmartMap.v +++ b/src/Reflection/Named/ContextProperties/SmartMap.v @@ -25,7 +25,7 @@ Section with_context. (H1 : @find_Name_and_val var' t n T N V1 None = Some v1) (H2 : @find_Name_and_val var'' t n T N V2 None = Some v2) : List.In (existT (fun t => (var' t * var'' t)%type) t (v1, v2)) (Wf.flatten_binding_list V1 V2). - Proof. + Proof using Type. induction T; [ | | specialize (IHT1 (fst N) (fst V1) (fst V2)); specialize (IHT2 (snd N) (snd V1) (snd V2)) ]; @@ -38,7 +38,7 @@ Section with_context. : @find_Name n (SmartFlatTypeMap f (t:=T) V) (SmartFlatTypeMapInterp2 (var':=var') (fun _ _ (n' : Name) => n') V N) = None <-> find_Name n N = None. - Proof. + Proof using Type. split; (induction T; [ | | specialize (IHT1 (fst V) (fst N)); @@ -50,19 +50,19 @@ Section with_context. : @find_Name n (SmartFlatTypeMap f (t:=T) V) (SmartFlatTypeMapInterp2 (var':=var') (fun _ _ (n' : Name) => n') V N) = None -> find_Name n N = None. - Proof. apply find_Name_SmartFlatTypeMapInterp2_None_iff. Qed. + Proof using Type. apply find_Name_SmartFlatTypeMapInterp2_None_iff. Qed. Hint Rewrite @find_Name_SmartFlatTypeMapInterp2_None using eassumption : ctx_db. Lemma find_Name_SmartFlatTypeMapInterp2_None' {var' n f T V N} : find_Name n N = None -> @find_Name n (SmartFlatTypeMap f (t:=T) V) (SmartFlatTypeMapInterp2 (var':=var') (fun _ _ (n' : Name) => n') V N) = None. - Proof. apply find_Name_SmartFlatTypeMapInterp2_None_iff. Qed. + Proof using Type. apply find_Name_SmartFlatTypeMapInterp2_None_iff. Qed. Lemma find_Name_SmartFlatTypeMapInterp2_None_Some_wrong {var' n f T V N v} : @find_Name n (SmartFlatTypeMap f (t:=T) V) (SmartFlatTypeMapInterp2 (var':=var') (fun _ _ (n' : Name) => n') V N) = None -> find_Name n N = Some v -> False. - Proof. + Proof using Type. intro; erewrite find_Name_SmartFlatTypeMapInterp2_None by eassumption; congruence. Qed. Local Hint Resolve @find_Name_SmartFlatTypeMapInterp2_None_Some_wrong. @@ -77,7 +77,7 @@ Section with_context. end | None => None end. - Proof. + Proof using Type. induction T; [ | | specialize (IHT1 (fst V) (fst N)); specialize (IHT2 (snd V) (snd N)) ]. @@ -110,7 +110,7 @@ Section with_context. -> @find_Name_and_val var''' t n T N (SmartFlatTypeMapUnInterp (f:=f) g X) None = Some v' -> g t b v = v'. - Proof. + Proof using Type. induction T; [ | | specialize (IHT1 (fst V) (fst N) (fst X)); specialize (IHT2 (snd V) (snd N) (snd X)) ]; @@ -134,7 +134,7 @@ Section with_context. -> @find_Name_and_val var''' t n T N (SmartFlatTypeMapUnInterp (f:=f) g X) None = Some v' -> g t b v = v'. - Proof. + Proof using Type. induction T; [ | | specialize (IHT1 (fst V) (fst N) (fst X)); specialize (IHT2 (snd V) (snd N) (snd X)) ]; @@ -154,7 +154,7 @@ Section with_context. (H1 : @find_Name_and_val var'' t n T N y None = Some v1) (HR : interp_flat_type_rel_pointwise R x y) : R _ v0 v1. - Proof. + Proof using Type. induction T; [ | | specialize (IHT1 (fst N) (fst x) (fst y)); specialize (IHT2 (snd N) (snd x) (snd y)) ]; @@ -182,7 +182,7 @@ Section with_context. :> { b : _ & var'' (f _ b)}) (N' := SmartFlatTypeMapInterp2 (var'':=fun _ => Name) (f:=f) (fun _ _ n => n) _ N) : b = h v /\ find_Name_and_val (f t (h v)) n N' V None = Some (i v). - Proof. + Proof using Type. induction T; [ | | specialize (IHT1 (fst N) (fst B) (fst V)); specialize (IHT2 (snd N) (snd B) (snd V)) ]; diff --git a/src/Reflection/Named/FMapContext.v b/src/Reflection/Named/FMapContext.v index b838c1b4f..e01186f2c 100644 --- a/src/Reflection/Named/FMapContext.v +++ b/src/Reflection/Named/FMapContext.v @@ -37,7 +37,7 @@ Module FMapContextFun (E : DecidableType) (W : WSfun E). := W.remove n ctx; empty := W.empty _ |}. Lemma FMapContextOk : @ContextOk base_type_code W.key var FMapContext. - Proof. + Proof using E_eq_l base_type_code_lb. split; repeat first [ reflexivity | progress simpl in * diff --git a/src/Reflection/Named/InterpretToPHOASInterp.v b/src/Reflection/Named/InterpretToPHOASInterp.v index 7dcdc198b..4f66e94d4 100644 --- a/src/Reflection/Named/InterpretToPHOASInterp.v +++ b/src/Reflection/Named/InterpretToPHOASInterp.v @@ -30,7 +30,7 @@ Section language. (Hwf : prop_of_option (Named.wff ctx e)) : Named.interpf (interp_op:=interp_op) (ctx:=ctx) e = Some (Syntax.interpf interp_op (interpf_to_phoas failb ctx e)). - Proof. + Proof using Type. revert dependent ctx; induction e; repeat first [ progress intros | progress subst @@ -58,7 +58,7 @@ Section language. v : Named.interp (interp_op:=interp_op) (ctx:=ctx) e v = Some (Syntax.interp interp_op (interp_to_phoas failb ctx e) v). - Proof. + Proof using Type. unfold interp, interp_to_phoas, Named.interp; apply interpf_interpf_to_phoas; auto. Qed. End with_context. @@ -75,7 +75,7 @@ Section language. v : Named.interp (interp_op:=interp_op) (ctx:=ctx _) e v = Some (Interp interp_op (InterpToPHOAS_gen failb ctx e) v). - Proof. apply interp_interp_to_phoas; auto. Qed. + Proof using Type. apply interp_interp_to_phoas; auto. Qed. Lemma Interp_InterpToPHOAS {t} (e : @Named.expr base_type_code op Name t) @@ -83,6 +83,6 @@ Section language. v : Named.interp (Context:=Context _) (interp_op:=interp_op) (ctx:=empty) e v = Some (Interp interp_op (InterpToPHOAS (Context:=Context) failb e) v). - Proof. apply interp_interp_to_phoas; auto. Qed. + Proof using Type. apply interp_interp_to_phoas; auto. Qed. End all. End language. diff --git a/src/Reflection/Named/InterpretToPHOASWf.v b/src/Reflection/Named/InterpretToPHOASWf.v index 86887cdee..daab24b62 100644 --- a/src/Reflection/Named/InterpretToPHOASWf.v +++ b/src/Reflection/Named/InterpretToPHOASWf.v @@ -73,7 +73,7 @@ Section language. (Hctx1_ctx2 : forall n t, lookupb ctx1 n t = None <-> lookupb ctx2 n t = None) : wff G (interpf_to_phoas failb1 ctx1 e) (interpf_to_phoas failb2 ctx2 e). - Proof. + Proof using Context1Ok Context2Ok Name_dec base_type_code_dec. revert dependent G; revert dependent ctx1; revert dependent ctx2; induction e; repeat first [ progress intros | progress destruct_head' and @@ -95,7 +95,7 @@ Section language. (Hctx1 : forall n t, lookupb ctx1 n t = None) (Hctx2 : forall n t, lookupb ctx2 n t = None) : wf (interp_to_phoas failb1 ctx1 e) (interp_to_phoas failb2 ctx2 e). - Proof. + Proof using Context1Ok Context2Ok Name_dec base_type_code_dec. constructor; intros. apply wff_interpf_to_phoas; t. Qed. @@ -105,7 +105,7 @@ Section language. (Hwf1 : Named.wf (Context:=Context1) empty e) (Hwf2 : Named.wf (Context:=Context2) empty e) : wf (interp_to_phoas (Context:=Context1) failb1 empty e) (interp_to_phoas (Context:=Context2) failb2 empty e). - Proof. + Proof using Context1Ok Context2Ok Name_dec base_type_code_dec. apply wf_interp_to_phoas_gen; auto using lookupb_empty. Qed. End with_var. @@ -121,7 +121,7 @@ Section language. (Hctx : forall var n t, lookupb (ctx var) n t = None) (Hwf : forall var, Named.wf (ctx var) e) : Wf (InterpToPHOAS_gen failb ctx e). - Proof. + Proof using ContextOk Name_dec base_type_code_dec. intros ??; apply wf_interp_to_phoas_gen; auto. Qed. @@ -129,7 +129,7 @@ Section language. {t} (e : @Named.expr base_type_code op Name t) (Hwf : Named.Wf Context e) : Wf (InterpToPHOAS (Context:=Context) failb e). - Proof. + Proof using ContextOk Name_dec base_type_code_dec. intros ??; apply wf_interp_to_phoas; auto. Qed. End all. diff --git a/src/Reflection/Named/MapCastInterp.v b/src/Reflection/Named/MapCastInterp.v index 1fe175879..b7afa1494 100644 --- a/src/Reflection/Named/MapCastInterp.v +++ b/src/Reflection/Named/MapCastInterp.v @@ -210,7 +210,7 @@ Section language. r' (Hr':interpf (interp_op:=interp_op) (ctx:=newValues) e' = Some r') , interpf (interp_op:=interp_op_bounds) (ctx:=varBounds) e = Some b /\ @inbounds _ b r /\ cast_back _ _ r' = r. - Proof. + Proof using Type*. induction e; simpl interpf; simpl mapf_cast; unfold option_map, cast_back in *; intros; repeat (break_match_hyps; inversion_option; inversion_sigma; simpl in *; unfold option_map in *; subst; try tauto). { destruct (Hctx _ _ _ Hr) as [b' [Hb'[Hb'v[v'[Hv' Hv'v]]]]]; clear Hctx Hr; subst. @@ -254,7 +254,7 @@ Section language. r' (Hr':interp (interp_op:=interp_op) (ctx:=newValues) e' v' = Some r') , interp (interp_op:=interp_op_bounds) (ctx:=varBounds) e input_bounds = Some b /\ @inbounds _ b r /\ cast_back _ _ r' = r. - Proof. + Proof using Type*. unfold map_cast, option_map, interp; simpl; intros. repeat first [ progress subst | progress inversion_option diff --git a/src/Reflection/Named/MapCastWf.v b/src/Reflection/Named/MapCastWf.v index a3196dbcc..f05df34c1 100644 --- a/src/Reflection/Named/MapCastWf.v +++ b/src/Reflection/Named/MapCastWf.v @@ -227,7 +227,7 @@ Section language. (Hb : find_Name_and_val base_type_dec Name_dec t n N B None = Some b) (N' := SmartFlatTypeMapInterp2 (var'':=fun _ => Name) (f:=pick_typeb) (fun _ _ n => n) _ N) : b = projT1 v /\ find_Name_and_val base_type_dec Name_dec (pick_typeb t (projT1 v)) n N' V None = Some (projT2 v). - Proof. + Proof using Type. eapply (find_Name_and_val_SmartFlatTypeMapUnInterp2_Some_Some base_type_dec Name_dec (h:=@projT1 _ _) (i:=@projT2 _ _) (f:=pick_typeb) (g:=fun _ => existT _)); auto. Qed. @@ -254,7 +254,7 @@ Section language. -> lookupb (t:=t) varBounds n = Some (projT1 v) /\ lookupb (t:=pick_typeb t (projT1 v)) newValues n = Some (projT2 v)), prop_of_option (Named.wff newValues e'). - Proof. induction e; t. Qed. + Proof using BoundsContextOk ContextOk FullContextOk Name_dec base_type_dec. induction e; t. Qed. Lemma wf_map_cast {t} (e:expr base_type_code op Name t) @@ -270,7 +270,7 @@ Section language. -> lookupb (t:=t) varBounds n = Some (projT1 v) /\ lookupb (t:=pick_typeb t (projT1 v)) newValues n = Some (projT2 v)), Named.wf newValues e'. - Proof. + Proof using BoundsContextOk ContextOk FullContextOk Name_dec base_type_dec. unfold Named.wf, map_cast, option_map, interp; simpl; intros. repeat first [ progress subst | progress inversion_option diff --git a/src/Reflection/Named/NameUtilProperties.v b/src/Reflection/Named/NameUtilProperties.v index 8dcf32ec5..9a52ff49d 100644 --- a/src/Reflection/Named/NameUtilProperties.v +++ b/src/Reflection/Named/NameUtilProperties.v @@ -27,7 +27,7 @@ Section language. : split_mnames force t ls = (fst (split_mnames force t (firstn (count_pairs t) ls)), skipn (count_pairs t) ls). - Proof. + Proof using Type. apply path_prod_uncurried; simpl. revert ls; induction t; split; split_prod; repeat first [ progress simpl in * @@ -56,17 +56,17 @@ Section language. Lemma snd_split_mnames_skipn (t : flat_type base_type_code) (ls : list MName) : snd (split_mnames force t ls) = skipn (count_pairs t) ls. - Proof. rewrite split_mnames_firstn_skipn; reflexivity. Qed. + Proof using Type. rewrite split_mnames_firstn_skipn; reflexivity. Qed. Lemma fst_split_mnames_firstn (t : flat_type base_type_code) (ls : list MName) : fst (split_mnames force t ls) = fst (split_mnames force t (firstn (count_pairs t) ls)). - Proof. rewrite split_mnames_firstn_skipn at 1; reflexivity. Qed. + Proof using Type. rewrite split_mnames_firstn_skipn at 1; reflexivity. Qed. Lemma mname_list_unique_firstn_skipn n ls : mname_list_unique force ls -> (mname_list_unique force (firstn n ls) /\ mname_list_unique force (skipn n ls)). - Proof. + Proof using Type. unfold mname_list_unique; intro H; split; intros k N; rewrite <- ?firstn_map, <- ?skipn_map, ?skipn_skipn, ?firstn_firstn_min, ?firstn_skipn_add; intros; eapply H; try eassumption. @@ -85,7 +85,7 @@ Section language. := fun H => proj2 (@mname_list_unique_firstn_skipn n ls H). Lemma mname_list_unique_nil : mname_list_unique force nil. - Proof. + Proof using Type. unfold mname_list_unique; simpl; intros ??. rewrite firstn_nil, skipn_nil; simpl; auto. Qed. @@ -96,29 +96,29 @@ Section language. : split_onames t ls = (fst (split_onames t (firstn (count_pairs t) ls)), skipn (count_pairs t) ls). - Proof. apply split_mnames_firstn_skipn. Qed. + Proof using Type. apply split_mnames_firstn_skipn. Qed. Lemma snd_split_onames_skipn (t : flat_type base_type_code) (ls : list (option Name)) : snd (split_onames t ls) = skipn (count_pairs t) ls. - Proof. apply snd_split_mnames_skipn. Qed. + Proof using Type. apply snd_split_mnames_skipn. Qed. Lemma fst_split_onames_firstn (t : flat_type base_type_code) (ls : list (option Name)) : fst (split_onames t ls) = fst (split_onames t (firstn (count_pairs t) ls)). - Proof. apply fst_split_mnames_firstn. Qed. + Proof using Type. apply fst_split_mnames_firstn. Qed. Lemma oname_list_unique_firstn n (ls : list (option Name)) : oname_list_unique ls -> oname_list_unique (firstn n ls). - Proof. apply mname_list_unique_firstn. Qed. + Proof using Type. apply mname_list_unique_firstn. Qed. Lemma oname_list_unique_skipn n (ls : list (option Name)) : oname_list_unique ls -> oname_list_unique (skipn n ls). - Proof. apply mname_list_unique_skipn. Qed. + Proof using Type. apply mname_list_unique_skipn. Qed. Lemma oname_list_unique_specialize (ls : list (option Name)) : oname_list_unique ls -> forall k n, List.In (Some n) (firstn k ls) -> List.In (Some n) (skipn k ls) -> False. - Proof. + Proof using Type. intros H k n; specialize (H k n). rewrite map_id in H; assumption. Qed. @@ -131,25 +131,25 @@ Section language. : split_names t ls = (fst (split_names t (firstn (count_pairs t) ls)), skipn (count_pairs t) ls). - Proof. apply split_mnames_firstn_skipn. Qed. + Proof using Type. apply split_mnames_firstn_skipn. Qed. Lemma snd_split_names_skipn (t : flat_type base_type_code) (ls : list Name) : snd (split_names t ls) = skipn (count_pairs t) ls. - Proof. apply snd_split_mnames_skipn. Qed. + Proof using Type. apply snd_split_mnames_skipn. Qed. Lemma fst_split_names_firstn (t : flat_type base_type_code) (ls : list Name) : fst (split_names t ls) = fst (split_names t (firstn (count_pairs t) ls)). - Proof. apply fst_split_mnames_firstn. Qed. + Proof using Type. apply fst_split_mnames_firstn. Qed. Lemma name_list_unique_firstn n (ls : list Name) : name_list_unique ls -> name_list_unique (firstn n ls). - Proof. + Proof using Type. unfold name_list_unique; intro H; apply oname_list_unique_firstn with (n:=n) in H. rewrite <- firstn_map; assumption. Qed. Lemma name_list_unique_skipn n (ls : list Name) : name_list_unique ls -> name_list_unique (skipn n ls). - Proof. + Proof using Type. unfold name_list_unique; intro H; apply oname_list_unique_skipn with (n:=n) in H. rewrite <- skipn_map; assumption. Qed. @@ -159,7 +159,7 @@ Section language. List.In n (firstn k ls) -> List.In n (skipn k ls) -> False. - Proof. + Proof using Type. intros H k n; specialize (H k n). rewrite !map_id, !firstn_map, !skipn_map in H. eauto using in_map. @@ -170,7 +170,7 @@ Section language. Lemma length_fst_split_names_Some_iff (t : flat_type base_type_code) (ls : list Name) : fst (split_names t ls) <> None <-> List.length ls >= count_pairs t. - Proof. + Proof using Type. revert ls; induction t; intros; try solve [ destruct ls; simpl; intuition (omega || congruence) ]. repeat first [ progress simpl in * @@ -195,7 +195,7 @@ Section language. Lemma length_fst_split_names_None_iff (t : flat_type base_type_code) (ls : list Name) : fst (split_names t ls) = None <-> List.length ls < count_pairs t. - Proof. + Proof using Type. destruct (length_fst_split_names_Some_iff t ls). destruct (le_lt_dec (count_pairs t) (List.length ls)); specialize_by omega; destruct (fst (split_names t ls)); split; try intuition (congruence || omega). @@ -204,7 +204,7 @@ Section language. Lemma split_onames_split_names (t : flat_type base_type_code) (ls : list Name) : split_onames t (List.map Some ls) = (fst (split_names t ls), List.map Some (snd (split_names t ls))). - Proof. + Proof using Type. revert ls; induction t; try solve [ destruct ls; reflexivity ]. repeat first [ progress simpl in * diff --git a/src/Reflection/Named/PositiveContext/DefaultsProperties.v b/src/Reflection/Named/PositiveContext/DefaultsProperties.v index 0fb1254ce..435a4c74c 100644 --- a/src/Reflection/Named/PositiveContext/DefaultsProperties.v +++ b/src/Reflection/Named/PositiveContext/DefaultsProperties.v @@ -16,7 +16,7 @@ Section language. Lemma name_list_unique_map_pos_of_succ_nat_seq a b : name_list_unique (map BinPos.Pos.of_succ_nat (seq a b)). - Proof. + Proof using Type. unfold name_list_unique, oname_list_unique, mname_list_unique. intros k n. rewrite !map_map, firstn_map, skipn_map, firstn_seq, skipn_seq. @@ -28,11 +28,11 @@ Section language. Lemma name_list_unique_default_names_forf {var dummy t e} : name_list_unique (@default_names_forf base_type_code op var dummy t e). - Proof. apply name_list_unique_map_pos_of_succ_nat_seq. Qed. + Proof using Type. apply name_list_unique_map_pos_of_succ_nat_seq. Qed. Lemma name_list_unique_default_names_for {var dummy t e} : name_list_unique (@default_names_for base_type_code op var dummy t e). - Proof. apply name_list_unique_map_pos_of_succ_nat_seq. Qed. + Proof using Type. apply name_list_unique_map_pos_of_succ_nat_seq. Qed. Lemma name_list_unique_DefaultNamesFor {t e} : name_list_unique (@DefaultNamesFor base_type_code op t e). - Proof. apply name_list_unique_map_pos_of_succ_nat_seq. Qed. + Proof using Type. apply name_list_unique_map_pos_of_succ_nat_seq. Qed. End language. diff --git a/src/Reflection/Named/WfInterp.v b/src/Reflection/Named/WfInterp.v index 17fc43ca5..c5fe2bb3a 100644 --- a/src/Reflection/Named/WfInterp.v +++ b/src/Reflection/Named/WfInterp.v @@ -15,7 +15,7 @@ Section language. Lemma wff_interpf_not_None {ctx : Context} {t} {e : @exprf base_type_code op Name t} (Hwf : prop_of_option (wff ctx e)) : @interpf base_type_code interp_base_type op Name Context interp_op ctx t e <> None. - Proof. + Proof using Type. revert dependent ctx; induction e; repeat first [ progress intros | progress simpl in * @@ -34,7 +34,7 @@ Section language. (Hwf : wf ctx e) v : @interp base_type_code interp_base_type op Name Context interp_op ctx t e v <> None. - Proof. + Proof using Type. destruct e; unfold interp, wf in *; apply wff_interpf_not_None; auto. Qed. End language. diff --git a/src/Reflection/Relations.v b/src/Reflection/Relations.v index 8ea1eaf18..9a927243d 100644 --- a/src/Reflection/Relations.v +++ b/src/Reflection/Relations.v @@ -88,7 +88,7 @@ Section language. Global Arguments interp_flat_type_rel_pointwise1 _ !_ _ / . Lemma interp_flat_type_rel_pointwise1_iff_relb {R} t x : interp_flat_type_relb_pointwise1 R t x <-> interp_flat_type_rel_pointwise1 R t x. - Proof. clear; induction t; rel_relb_t. Qed. + Proof using Type. clear; induction t; rel_relb_t. Qed. Definition interp_flat_type_rel_pointwise1_gen_Prop_iff_bool : forall {R} t x, interp_flat_type_rel_pointwise1_gen_Prop bool _ _ R t x @@ -102,7 +102,7 @@ Section language. Global Arguments interp_flat_type_rel_pointwise _ !_ _ _ / . Lemma interp_flat_type_rel_pointwise_iff_relb {R} t x y : interp_flat_type_relb_pointwise R t x y <-> interp_flat_type_rel_pointwise R t x y. - Proof. clear; induction t; rel_relb_t. Qed. + Proof using Type. clear; induction t; rel_relb_t. Qed. Definition interp_flat_type_rel_pointwise_gen_Prop_iff_bool : forall {R} t x y, interp_flat_type_rel_pointwise_gen_Prop bool _ _ R t x y @@ -116,7 +116,7 @@ Section language. Global Arguments interp_flat_type_rel_pointwise_hetero _ !_ !_ _ _ / . Lemma interp_flat_type_rel_pointwise_hetero_iff_relb {R} t1 t2 x y : interp_flat_type_relb_pointwise_hetero R t1 t2 x y <-> interp_flat_type_rel_pointwise_hetero R t1 t2 x y. - Proof. clear; revert dependent t2; induction t1, t2; rel_relb_t. Qed. + Proof using Type. clear; revert dependent t2; induction t1, t2; rel_relb_t. Qed. Definition interp_flat_type_rel_pointwise_hetero_gen_Prop_iff_bool : forall {R} t1 t2 x y, interp_flat_type_rel_pointwise_hetero_gen_Prop bool _ _ _ R t1 t2 x y @@ -126,18 +126,18 @@ Section language. Lemma interp_flat_type_rel_pointwise_hetero_iff {R t} x y : interp_flat_type_rel_pointwise (fun t => R t t) t x y <-> interp_flat_type_rel_pointwise_hetero R t t x y. - Proof. induction t; simpl; rewrite_hyp ?*; reflexivity. Qed. + Proof using Type. induction t; simpl; rewrite_hyp ?*; reflexivity. Qed. Lemma interp_flat_type_rel_pointwise_impl {R1 R2 : forall t, _ -> _ -> Prop} t x y : interp_flat_type_rel_pointwise (fun t x y => (R1 t x y -> R2 t x y)%type) t x y -> (interp_flat_type_rel_pointwise R1 t x y -> interp_flat_type_rel_pointwise R2 t x y). - Proof. induction t; simpl; intuition. Qed. + Proof using Type. induction t; simpl; intuition. Qed. Lemma interp_flat_type_rel_pointwise_always {R : forall t, _ -> _ -> Prop} : (forall t x y, R t x y) -> forall t x y, interp_flat_type_rel_pointwise R t x y. - Proof. induction t; simpl; intuition. Qed. + Proof using Type. induction t; simpl; intuition. Qed. End flat_type. Section flat_type_extra. Context {interp_base_type1 interp_base_type2 : base_type_code -> Type}. @@ -147,11 +147,11 @@ Section language. (fun t x y => (R1 t y x -> R2 t x y)%type) t x y -> (interp_flat_type_rel_pointwise R1 t y x -> interp_flat_type_rel_pointwise R2 t x y). - Proof. induction t; simpl; intuition. Qed. + Proof using Type. induction t; simpl; intuition. Qed. Global Instance interp_flat_type_rel_pointwise_Reflexive {R : forall t, _ -> _ -> Prop} {H : forall t, Reflexive (R t)} : forall t, Reflexive (@interp_flat_type_rel_pointwise interp_base_type1 interp_base_type1 R t). - Proof. + Proof using Type. induction t; intro; simpl; try apply conj; try reflexivity. Qed. @@ -161,7 +161,7 @@ Section language. t f g x y : @interp_flat_type_rel_pointwise interp_base_type1 interp_base_type2 R t (SmartVarfMap f x) (SmartVarfMap g y) <-> @interp_flat_type_rel_pointwise interp_base_type1' interp_base_type2' (fun t x y => R t (f _ x) (g _ y)) t x y. - Proof. + Proof using Type. induction t; simpl; try reflexivity. rewrite_hyp <- !*; reflexivity. Qed. @@ -246,16 +246,16 @@ Section language. (RProd' : forall A B x y, R (Prod A B) x y -> R A (fst x) (fst y) /\ R B (snd x) (snd y)). Lemma lift_interp_flat_type_rel_pointwise1 t (x : interp_flat_type1 t) (y : interp_flat_type2 t) : interp_flat_type_rel_pointwise R t x y -> R t x y. - Proof. clear RProd'; induction t; simpl; destruct_head_hnf' unit; intuition. Qed. + Proof using RProd RUnit. clear RProd'; induction t; simpl; destruct_head_hnf' unit; intuition. Qed. Lemma lift_interp_flat_type_rel_pointwise2 t (x : interp_flat_type1 t) (y : interp_flat_type2 t) : R t x y -> interp_flat_type_rel_pointwise R t x y. - Proof. clear RProd; induction t; simpl; destruct_head_hnf' unit; split_and; intuition. Qed. + Proof using RProd'. clear RProd; induction t; simpl; destruct_head_hnf' unit; split_and; intuition. Qed. End RProd. Section RProd_iff. Context (RProd : forall A B x y, R A (fst x) (fst y) /\ R B (snd x) (snd y) <-> R (Prod A B) x y). Lemma lift_interp_flat_type_rel_pointwise t (x : interp_flat_type1 t) (y : interp_flat_type2 t) : interp_flat_type_rel_pointwise R t x y <-> R t x y. - Proof. + Proof using RProd RUnit. split_iff; split; auto using lift_interp_flat_type_rel_pointwise1, lift_interp_flat_type_rel_pointwise2. Qed. End RProd_iff. @@ -266,7 +266,7 @@ Section language. (fun t x y => f t x = g t y) t x y <-> SmartVarfMap f x = SmartVarfMap g y. - Proof. + Proof using Type. induction t; unfold SmartVarfMap in *; simpl in *; destruct_head_hnf unit; try tauto. rewrite_hyp !*; intuition congruence. Qed. @@ -276,21 +276,21 @@ Section language. (fun t x y => x = f t y) t x y <-> x = SmartVarfMap f y. - Proof. rewrite lift_interp_flat_type_rel_pointwise_f_eq, SmartVarfMap_id; reflexivity. Qed. + Proof using Type. rewrite lift_interp_flat_type_rel_pointwise_f_eq, SmartVarfMap_id; reflexivity. Qed. Lemma lift_interp_flat_type_rel_pointwise_f_eq_id2 (f : forall t, _ -> _) t x y : @interp_flat_type_rel_pointwise interp_base_type1 interp_base_type2 (fun t x y => f t x = y) t x y <-> SmartVarfMap f x = y. - Proof. rewrite lift_interp_flat_type_rel_pointwise_f_eq, SmartVarfMap_id; reflexivity. Qed. + Proof using Type. rewrite lift_interp_flat_type_rel_pointwise_f_eq, SmartVarfMap_id; reflexivity. Qed. Lemma lift_interp_flat_type_rel_pointwise_f_eq2 {T} (f g : forall t, _ -> _ -> T t) t x y : @interp_flat_type_rel_pointwise interp_base_type1 interp_base_type2 (fun t x y => f t x y = g t x y) t x y <-> SmartVarfMap2 f x y = SmartVarfMap2 g x y. - Proof. + Proof using Type. induction t; unfold SmartVarfMap2 in *; simpl in *; destruct_head_hnf unit; try tauto. rewrite_hyp !*; intuition congruence. Qed. @@ -300,7 +300,7 @@ Section language. (fun t x y => f t x = g t y) t x y <-> (forall a b, SmartVarfMap f a = SmartVarfMap g b -> SmartVarfMap f (x a) = SmartVarfMap g (y b)). - Proof. + Proof using Type. destruct t; simpl; unfold interp_type_rel_pointwise, respectful_hetero. setoid_rewrite lift_interp_flat_type_rel_pointwise_f_eq; reflexivity. Qed. @@ -310,14 +310,14 @@ Section language. (fun t x y => x = f t y) t x y <-> (forall a, x (SmartVarfMap f a) = SmartVarfMap f (y a)). - Proof. rewrite lift_interp_type_rel_pointwise_f_eq; setoid_rewrite SmartVarfMap_id; firstorder (subst; eauto). Qed. + Proof using Type. rewrite lift_interp_type_rel_pointwise_f_eq; setoid_rewrite SmartVarfMap_id; firstorder (subst; eauto). Qed. Lemma lift_interp_type_rel_pointwise_f_eq_id2 (f : forall t, _ -> _) t x y : interp_type_rel_pointwise interp_base_type1 interp_base_type2 (fun t x y => f t x = y) t x y <-> (forall a, SmartVarfMap f (x a) = y (SmartVarfMap f a)). - Proof. rewrite lift_interp_type_rel_pointwise_f_eq; setoid_rewrite SmartVarfMap_id; firstorder (subst; eauto). Qed. + Proof using Type. rewrite lift_interp_type_rel_pointwise_f_eq; setoid_rewrite SmartVarfMap_id; firstorder (subst; eauto). Qed. End lifting. Local Ltac t := @@ -341,14 +341,14 @@ Section language. (H : List.In (existT _ t (v1, v2)%core) (flatten_binding_list e1 e2)) (HR : @interp_flat_type_rel_pointwise interp_base_type1 interp_base_type2 R' T e1 e2) : R' t v1 v2. - Proof. induction T; t. Qed. + Proof using Type. induction T; t. Qed. Lemma interp_flat_type_rel_pointwise_hetero_flatten_binding_list2 {interp_base_type1 interp_base_type2 t1 t2 T1 T2} R' e1 e2 v1 v2 (H : List.In (existT _ (t1, t2)%core (v1, v2)%core) (flatten_binding_list2 e1 e2)) (HR : @interp_flat_type_rel_pointwise_hetero interp_base_type1 interp_base_type2 R' T1 T2 e1 e2) : R' t1 t2 v1 v2. - Proof. + Proof using Type. revert dependent T2; induction T1, T2; t. Qed. End language. diff --git a/src/Reflection/RewriterInterp.v b/src/Reflection/RewriterInterp.v index 66315ec0d..4a18c0a47 100644 --- a/src/Reflection/RewriterInterp.v +++ b/src/Reflection/RewriterInterp.v @@ -24,13 +24,13 @@ Section language. Lemma interpf_rewrite_opf {t} (e : exprf t) : interpf interp_op (rewrite_opf rewrite_op_expr e) = interpf interp_op e. - Proof. + Proof using Type*. induction e; simpl; unfold LetIn.Let_In; rewrite_hyp ?*; reflexivity. Qed. Lemma interp_rewrite_op {t} (e : expr t) : forall x, interp interp_op (rewrite_op rewrite_op_expr e) x = interp interp_op e x. - Proof. + Proof using Type*. destruct e; intro x; apply interpf_rewrite_opf. Qed. End specialized. @@ -42,7 +42,7 @@ Section language. = interp_op _ _ opc (interpf interp_op args)) {t} (e : Expr t) : forall x, Interp interp_op (RewriteOp rewrite_op_expr e) x = Interp interp_op e x. - Proof. + Proof using Type. apply interp_rewrite_op; assumption. Qed. End language. diff --git a/src/Reflection/RewriterWf.v b/src/Reflection/RewriterWf.v index a9ad229a0..a7ac86851 100644 --- a/src/Reflection/RewriterWf.v +++ b/src/Reflection/RewriterWf.v @@ -31,14 +31,14 @@ Section language. Lemma wff_rewrite_opf {t} G (e1 : @exprf var1 t) (e2 : @exprf var2 t) (Hwf : wff G e1 e2) : wff G (rewrite_opf rewrite_op_expr1 e1) (rewrite_opf rewrite_op_expr2 e2). - Proof. + Proof using Type*. induction Hwf; simpl; try constructor; auto. Qed. Lemma wf_rewrite_opf {t} (e1 : @expr var1 t) (e2 : @expr var2 t) (Hwf : wf e1 e2) : wf (rewrite_op rewrite_op_expr1 e1) (rewrite_op rewrite_op_expr2 e2). - Proof. + Proof using Type*. destruct Hwf; simpl; constructor; intros; apply wff_rewrite_opf; auto. Qed. End with_var. @@ -53,7 +53,7 @@ Section language. {t} (e : Expr t) (Hwf : Wf e) : Wf (RewriteOp rewrite_op_expr e). - Proof. + Proof using Type. intros var1 var2; apply wf_rewrite_opf; auto. Qed. End language. diff --git a/src/Reflection/SmartBoundInterp.v b/src/Reflection/SmartBoundInterp.v index 7723d98c4..0262ef615 100644 --- a/src/Reflection/SmartBoundInterp.v +++ b/src/Reflection/SmartBoundInterp.v @@ -72,13 +72,13 @@ Section language. {t} e bounds : interpf interp_op (SmartPairf (interpf_smart_bound_exprf (t:=t) e bounds)) = interpf_smart_bound e bounds. - Proof. clear -interpf_cast; induction t; t. Qed. + Proof using interpf_cast. clear -interpf_cast; induction t; t. Qed. Lemma interpf_SmartPairf_interpf_smart_unbound_exprf {t} bounds e : interpf interp_op (SmartPairf (interpf_smart_unbound_exprf (t:=t) bounds e)) = interpf_smart_unbound bounds (SmartVarfMap (fun _ e => interpf interp_op e) e). - Proof. clear -interpf_cast; induction t; t. Qed. + Proof using interpf_cast. clear -interpf_cast; induction t; t. Qed. Lemma interp_smart_bound_and_rel {t} (e : expr t) (ebounds : expr t) @@ -91,7 +91,7 @@ Section language. -> is_bounded_by (interp interp_op e (interpf_smart_unbound input_bounds x)) output_bounds /\ interpf_smart_unbound _ (interp interp_op e' x) = interp interp_op e (interpf_smart_unbound input_bounds x). - Proof. + Proof using interpf_cast is_bounded_by_interp_op strip_cast_val. intros; subst e' output_bounds. match goal with |- ?A /\ ?B => cut (A /\ (A -> B)); [ tauto | ] end. split. @@ -121,7 +121,7 @@ Section language. -> is_bounded_by (Interp interp_op e (interpf_smart_unbound input_bounds x)) output_bounds /\ interpf_smart_unbound _ (Interp interp_op e' x) = Interp interp_op e (interpf_smart_unbound input_bounds x). - Proof. + Proof using interpf_cast is_bounded_by_interp_op strip_cast_val. apply interp_smart_bound_and_rel; auto. Qed. @@ -138,7 +138,7 @@ Section language. is_bounded_by (interpf_smart_unbound input_bounds x) input_bounds -> interpf_smart_unbound _ (Interp interp_op e' x) = Interp interp_op e (interpf_smart_unbound input_bounds x). - Proof. + Proof using interpf_cast is_bounded_by_interp_op strip_cast_val. intros; eapply InterpSmartBoundAndRel; auto. Qed. End language. diff --git a/src/Reflection/SmartBoundWf.v b/src/Reflection/SmartBoundWf.v index 6c2846337..72c5c1475 100644 --- a/src/Reflection/SmartBoundWf.v +++ b/src/Reflection/SmartBoundWf.v @@ -44,7 +44,7 @@ Section language. : wff G (@bound_op ovar1 src1 dst1 src2 dst2 opc1 opc2 e1 args2) (@bound_op ovar2 src1 dst1 src2 dst2 opc1 opc2 e2 args2). - Proof. + Proof using wff_Cast. unfold SmartBound.bound_op; repeat first [ progress break_innermost_match | assumption @@ -73,7 +73,7 @@ Section language. (t:=t) (interpf_smart_unbound_exprf input_bounds (SmartVarfMap (fun t => Var) x2))). - Proof. + Proof using wff_Cast. clear -wff_Cast. unfold SmartPairf, SmartVarfMap, interpf_smart_unbound_exprf; induction t; repeat match goal with @@ -98,7 +98,7 @@ Section language. (SmartPairf (var:=var2) (interpf_smart_bound_exprf x2 output_bounds)). - Proof. + Proof using wff_Cast. clear -wff_Cast. unfold SmartPairf, SmartVarfMap, interpf_smart_bound_exprf; induction t; repeat match goal with @@ -119,7 +119,7 @@ Section language. (Hwf : wf e1 e2) : wf (@smart_bound var1 t1 e1 e_bounds input_bounds) (@smart_bound var2 t1 e2 e_bounds input_bounds). - Proof. + Proof using wff_Cast. clear -wff_Cast Hwf. destruct Hwf; unfold SmartBound.smart_bound. repeat constructor; auto with wf; intros; @@ -130,7 +130,7 @@ Section language. Lemma Wf_SmartBound {t1} e input_bounds (Hwf : Wf e) : Wf (@SmartBound t1 e input_bounds). - Proof. + Proof using wff_Cast. intros var1 var2; specialize (Hwf var1 var2). unfold SmartBound.SmartBound. apply wf_smart_bound; assumption. diff --git a/src/Reflection/SmartCastInterp.v b/src/Reflection/SmartCastInterp.v index 410d108e3..92ca265e1 100644 --- a/src/Reflection/SmartCastInterp.v +++ b/src/Reflection/SmartCastInterp.v @@ -24,7 +24,7 @@ Section language. Lemma interpf_SmartCast_base {A A'} (x : exprf (Tbase A)) : interpf interp_op (SmartCast_base x) = interpf interp_op (Cast _ A A' x). - Proof. + Proof using interpf_Cast_id. clear dependent cast_val. unfold SmartCast_base. destruct (Sumbool.sumbool_of_bool (base_type_beq A A')) as [H|H]. diff --git a/src/Reflection/SmartCastWf.v b/src/Reflection/SmartCastWf.v index ef5d0170d..4c5601669 100644 --- a/src/Reflection/SmartCastWf.v +++ b/src/Reflection/SmartCastWf.v @@ -27,7 +27,7 @@ Section language. Lemma wff_SmartCast_base {var1 var2 A A'} G e1 e2 (Hwf : wff (var1:=var1) (var2:=var2) G (t:=Tbase A) e1 e2) : wff G (t:=Tbase A') (SmartCast_base e1) (SmartCast_base e2). - Proof. + Proof using wff_Cast. unfold SmartCast_base; destruct (Sumbool.sumbool_of_bool (base_type_beq A A')) as [H|H]. { destruct (base_type_bl_transparent A A' H); assumption. } { auto. } @@ -44,7 +44,7 @@ Section language. | None, None => True | Some _, None | None, Some _ => False end. - Proof. + Proof using wff_Cast. break_innermost_match; revert dependent B; induction A, B; repeat match goal with | _ => progress simpl in * @@ -67,7 +67,7 @@ Section language. : SmartCast A B = Some f1 -> SmartCast A B = Some f2 -> forall e1 e2, wff (var1:=var1) (var2:=var2) (flatten_binding_list e1 e2) (f1 e1) (f2 e2). - Proof. + Proof using wff_Cast. intros H1 H2; generalize (@wff_SmartCast_match var1 var2 A B). rewrite H1, H2; trivial. Qed. @@ -76,7 +76,7 @@ Section language. : SmartCast A B = Some f1 -> SmartCast A B = Some f2 -> forall e1 e2, wff (var1:=var1) (var2:=var2) (flatten_binding_list e1 e2 ++ G) (f1 e1) (f2 e2). - Proof. + Proof using wff_Cast. intros; eapply wff_in_impl_Proper; [ eapply wff_SmartCast; eassumption | auto ]. Qed. End language. diff --git a/src/Reflection/SmartMap.v b/src/Reflection/SmartMap.v index 3f66c01d6..934497f65 100644 --- a/src/Reflection/SmartMap.v +++ b/src/Reflection/SmartMap.v @@ -95,7 +95,7 @@ Section homogenous_type. := @smart_interp_flat_map exprfb exprf (fun t x => x) TT (fun A B x y => Pair x y) t. Lemma SmartPairf_Pair {A B} (e1 : interp_flat_type _ A) (e2 : interp_flat_type _ B) : SmartPairf (t:=Prod A B) (e1, e2)%core = Pair (SmartPairf e1) (SmartPairf e2). - Proof. reflexivity. Qed. + Proof using Type. reflexivity. Qed. Definition SmartVarf {t} : interp_flat_type var t -> exprf t := @smart_interp_flat_map var exprf (fun t => Var) TT (fun A B x y => Pair x y) t. Definition SmartVarf_Pair {A B v} @@ -107,12 +107,12 @@ Section homogenous_type. Lemma SmartVarfMap_compose {var' var'' var''' t} f g x : @SmartVarfMap var'' var''' g t (@SmartVarfMap var' var'' f t x) = @SmartVarfMap _ _ (fun t v => g t (f t v)) t x. - Proof. + Proof using Type. unfold SmartVarfMap; clear; induction t; simpl; destruct_head_hnf unit; destruct_head_hnf prod; rewrite_hyp ?*; congruence. Qed. Lemma SmartVarfMap_id {var' t} x : @SmartVarfMap var' var' (fun _ x => x) t x = x. - Proof. + Proof using Type. unfold SmartVarfMap; clear; induction t; simpl; destruct_head_hnf unit; destruct_head_hnf prod; rewrite_hyp ?*; congruence. Qed. @@ -122,7 +122,7 @@ Section homogenous_type. ==> (forall_relation (fun A => forall_relation (fun B => pointwise_relation _ (pointwise_relation _ eq)))) ==> forall_relation (fun t => eq ==> eq)) (@smart_interp_flat_map f g). - Proof. + Proof using Type. unfold forall_relation, pointwise_relation, respectful. intros F G HFG x y ? Q R HQR t a b ?; subst y b. induction t; simpl in *; auto. @@ -131,7 +131,7 @@ Section homogenous_type. Global Instance SmartVarfMap_Proper {var' var''} : Proper (forall_relation (fun t => pointwise_relation _ eq) ==> forall_relation (fun t => eq ==> eq)) (@SmartVarfMap var' var''). - Proof. + Proof using Type. repeat intro; eapply smart_interp_flat_map_Proper; trivial; repeat intro; reflexivity. Qed. Definition SmartVarfMap2 {var var' var''} (f : forall t, var t -> var' t -> var'' t) {t} @@ -141,7 +141,7 @@ Section homogenous_type. (x : interp_flat_type var' t) (y : interp_flat_type var'' t) : SmartVarfMap2 (fun _ a b => a) x y = x. - Proof. + Proof using Type. unfold SmartVarfMap2; clear; induction t; simpl; destruct_head_hnf unit; destruct_head_hnf prod; rewrite_hyp ?*; congruence. Qed. @@ -149,7 +149,7 @@ Section homogenous_type. (x : interp_flat_type var' t) (y : interp_flat_type var'' t) : SmartVarfMap2 (fun _ a b => b) x y = y. - Proof. + Proof using Type. unfold SmartVarfMap2; clear; induction t; simpl; destruct_head_hnf unit; destruct_head_hnf prod; rewrite_hyp ?*; congruence. Qed. @@ -215,7 +215,7 @@ Section homogenous_type. | Arrow src dst => fun F x => SmartVarfMap f (F (SmartVarfMap f' x)) end. Lemma SmartVarMap_id {var' t} x v : @SmartVarMap var' var' (fun _ x => x) (fun _ x => x) t x v = x v. - Proof. destruct t; simpl; rewrite !SmartVarfMap_id; reflexivity. Qed. + Proof using Type. destruct t; simpl; rewrite !SmartVarfMap_id; reflexivity. Qed. Definition SmartVarVarf {t} : interp_flat_type var t -> interp_flat_type exprfb t := SmartVarfMap (fun t => Var). End homogenous_type. @@ -300,7 +300,7 @@ Section hetero_type. (@SmartFlatTypeMap2Interp2 _ _ _ f gv t v e) = SmartVarfMap2 (fun t v e => fv t v (gv t v e)) v e. - Proof. + Proof using Type. induction t; simpl in *; destruct_head' unit; rewrite_hyp ?*; reflexivity. Qed. diff --git a/src/Reflection/Tuple.v b/src/Reflection/Tuple.v index 6071f13c2..519325b82 100644 --- a/src/Reflection/Tuple.v +++ b/src/Reflection/Tuple.v @@ -34,16 +34,16 @@ Section language. end. Lemma flat_interp_untuple'_tuple' {T n v} : @flat_interp_untuple' T n (flat_interp_tuple' v) = v. - Proof. induction n; [ reflexivity | simpl; rewrite IHn; destruct v; reflexivity ]. Qed. + Proof using Type. induction n; [ reflexivity | simpl; rewrite IHn; destruct v; reflexivity ]. Qed. Lemma flat_interp_untuple_tuple {T n v} : flat_interp_untuple (@flat_interp_tuple T n v) = v. - Proof. destruct n; [ reflexivity | apply flat_interp_untuple'_tuple' ]. Qed. + Proof using Type. destruct n; [ reflexivity | apply flat_interp_untuple'_tuple' ]. Qed. Lemma flat_interp_tuple'_untuple' {T n v} : @flat_interp_tuple' T n (flat_interp_untuple' v) = v. - Proof. induction n; [ reflexivity | simpl; rewrite IHn; destruct v; reflexivity ]. Qed. + Proof using Type. induction n; [ reflexivity | simpl; rewrite IHn; destruct v; reflexivity ]. Qed. Lemma flat_interp_tuple_untuple {T n v} : @flat_interp_tuple T n (flat_interp_untuple v) = v. - Proof. destruct n; [ reflexivity | apply flat_interp_tuple'_untuple' ]. Qed. + Proof using Type. destruct n; [ reflexivity | apply flat_interp_tuple'_untuple' ]. Qed. Definition tuple_map {A B n} (f : interp_flat_type A -> interp_flat_type B) (v : interp_flat_type (tuple A n)) : interp_flat_type (tuple B n) diff --git a/src/Reflection/WfInversion.v b/src/Reflection/WfInversion.v index b8cb16c6a..d76fd90f4 100644 --- a/src/Reflection/WfInversion.v +++ b/src/Reflection/WfInversion.v @@ -103,12 +103,12 @@ Section language. Defined. Definition wff_endecode {G t e1 e2} v : @wff_decode G t e1 e2 (@wff_encode G t e1 e2 v) = v. - Proof. + Proof using Type. destruct v; reflexivity. Qed. Definition wff_deencode {G t e1 e2} v : @wff_encode G t e1 e2 (@wff_decode G t e1 e2 v) = v. - Proof. + Proof using Type. destruct e1; simpl in *; move e2 at top; lazymatch type of e2 with @@ -154,12 +154,12 @@ Section language. Defined. Definition wf_endecode {t e1 e2} v : @wf_decode t e1 e2 (@wf_encode t e1 e2 v) = v. - Proof. + Proof using Type. destruct v; reflexivity. Qed. Definition wf_deencode {t e1 e2} v : @wf_encode t e1 e2 (@wf_decode t e1 e2 v) = v. - Proof. + Proof using Type. destruct e1 as [src dst f1]. revert dependent f1. refine match e2 with diff --git a/src/Reflection/WfProofs.v b/src/Reflection/WfProofs.v index dcf3d8347..ca1f50478 100644 --- a/src/Reflection/WfProofs.v +++ b/src/Reflection/WfProofs.v @@ -27,7 +27,7 @@ Section language. Lemma wff_app' {g G0 G1 t e1 e2} (wf : @wff var1 var2 (G0 ++ G1) t e1 e2) : wff (G0 ++ g ++ G1) e1 e2. - Proof. + Proof using Type. rewrite !List.app_assoc. revert wf; remember (G0 ++ G1)%list as G eqn:?; intro wf. revert dependent G0. revert dependent G1. @@ -40,14 +40,14 @@ Section language. Lemma wff_app_pre {g G t e1 e2} (wf : @wff var1 var2 G t e1 e2) : wff (g ++ G) e1 e2. - Proof. + Proof using Type. apply (@wff_app' _ nil); assumption. Qed. Lemma wff_app_post {g G t e1 e2} (wf : @wff var1 var2 G t e1 e2) : wff (G ++ g) e1 e2. - Proof. + Proof using Type. pose proof (@wff_app' g G nil t e1 e2) as H. rewrite !List.app_nil_r in *; auto. Qed. @@ -56,7 +56,7 @@ Section language. : @wff var1 var2 G0 t e1 e2 -> (forall x, List.In x G0 -> List.In x G1) -> @wff var1 var2 G1 t e1 e2. - Proof. + Proof using Type. intro wf; revert G1; induction wf; repeat match goal with | _ => setoid_rewrite List.in_app_iff @@ -74,7 +74,7 @@ Section language. Lemma wff_SmartVarf {t} x1 x2 : @wff var1 var2 (flatten_binding_list x1 x2) t (SmartVarf x1) (SmartVarf x2). - Proof. + Proof using Type. unfold SmartVarf. induction t; simpl; constructor; eauto. Qed. @@ -85,7 +85,7 @@ Section language. (Hin : List.In (existT (fun t : base_type_code => (exprf (Tbase t) * exprf (Tbase t))%type) t (x1, x2)) (flatten_binding_list (SmartVarVarf v1) (SmartVarVarf v2))) : @wff var1 var2 (flatten_binding_list (t:=t') v1 v2 ++ G) (Tbase t) x1 x2. - Proof. + Proof using Type. revert dependent G; induction t'; intros; simpl in *; try tauto. { intuition (inversion_sigma; inversion_prod; subst; simpl; eauto). constructor; eauto. } @@ -99,7 +99,7 @@ Section language. (Hin : List.In (existT (fun t : base_type_code => (exprf (Tbase t) * exprf (Tbase t))%type) t (x1, x2)) (flatten_binding_list (SmartVarVarf v1) (SmartVarVarf v2))) : @wff var1 var2 (flatten_binding_list (t:=t') v1 v2) (Tbase t) x1 x2. - Proof. + Proof using Type. apply wff_SmartVarVarf with (G:=nil) in Hin. rewrite List.app_nil_r in Hin; assumption. Qed. @@ -108,7 +108,7 @@ Section language. (Hwf : @wff var1 var2 G t (SmartVarf v1) (SmartVarf v2)) (Hin : List.In e (flatten_binding_list v1 v2)) : List.In e G. - Proof. + Proof using Type. induction t; repeat match goal with | _ => assumption @@ -136,7 +136,7 @@ Section language. {var1 var2 t1} x1 x2 : duplicate_types (@flatten_binding_list base_type_code var1 var2 t1 x1 x2) = @flatten_binding_list2 base_type_code var1 var2 t1 t1 x1 x2. - Proof. + Proof using Type. induction t1; simpl; try reflexivity. rewrite_hyp <- !*. unfold duplicate_types; rewrite List.map_app; reflexivity. @@ -157,7 +157,7 @@ Section language. : flatten_binding_list2 (var1:=var1') (var2:=var2') (base_type_code:=base_type_code) (SmartVarfMap f x1) (SmartVarfMap g x2) = List.map (fun txy => existT _ (projT1 txy) (f _ (fst (projT2 txy)), g _ (snd (projT2 txy)))%core) (flatten_binding_list2 x1 x2). - Proof. + Proof using Type. revert dependent t2; induction t1, t2; flatten_t. Qed. @@ -166,7 +166,7 @@ Section language. : flatten_binding_list2 (var1:=var1') (var2:=var2') (base_type_code:=base_type_code) (SmartVarfMap f x1) x2 = List.map (fun txy => existT _ (projT1 txy) (f _ (fst (projT2 txy)), snd (projT2 txy))%core) (flatten_binding_list2 x1 x2). - Proof. + Proof using Type. revert dependent t2; induction t1, t2; flatten_t. Qed. @@ -175,7 +175,7 @@ Section language. : flatten_binding_list2 (var1:=var1') (var2:=var2') (base_type_code:=base_type_code) x1 (SmartVarfMap g x2) = List.map (fun txy => existT _ (projT1 txy) (fst (projT2 txy), g _ (snd (projT2 txy)))%core) (flatten_binding_list2 x1 x2). - Proof. + Proof using Type. revert dependent t2; induction t1, t2; flatten_t. Qed. @@ -184,14 +184,14 @@ Section language. : flatten_binding_list (var1:=var1') (var2:=var2') (base_type_code:=base_type_code) (SmartVarfMap f x1) (SmartVarfMap g x2) = List.map (fun txy => existT _ (projT1 txy) (f _ (fst (projT2 txy)), g _ (snd (projT2 txy)))%core) (flatten_binding_list x1 x2). - Proof. induction t; flatten_t. Qed. + Proof using Type. induction t; flatten_t. Qed. Lemma flatten_binding_list2_SmartValf {T1 T2} f g t1 t2 : flatten_binding_list2 (base_type_code:=base_type_code) (SmartValf T1 f t1) (SmartValf T2 g t2) = List.map (fun txy => existT _ (projT1 txy) (f _, g _)%core) (flatten_binding_list2 (SmartFlatTypeUnMap t1) (SmartFlatTypeUnMap t2)). - Proof. + Proof using Type. revert dependent t2; induction t1, t2; flatten_t. Qed. @@ -200,13 +200,13 @@ Section language. : flatten_binding_list (base_type_code:=base_type_code) (SmartValf T1 f t) (SmartValf T2 g t) = List.map (fun txy => existT _ (projT1 txy) (f _, g _)%core) (flatten_binding_list (SmartFlatTypeUnMap t) (SmartFlatTypeUnMap t)). - Proof. induction t; flatten_t. Qed. + Proof using Type. induction t; flatten_t. Qed. Lemma flatten_binding_list_In_eq_iff {var} T x y : (forall t a b, List.In (existT _ t (a, b)) (@flatten_binding_list base_type_code var var T x y) -> a = b) <-> x = y. - Proof. + Proof using Type. induction T; repeat first [ exfalso; assumption | progress subst @@ -231,7 +231,7 @@ Section language. Lemma flatten_binding_list_same_in_eq {var} {T x t a b} : List.In (existT _ t (a, b)) (@flatten_binding_list base_type_code var var T x x) -> a = b. - Proof. intro; eapply flatten_binding_list_In_eq_iff; eauto. Qed. + Proof using Type. intro; eapply flatten_binding_list_In_eq_iff; eauto. Qed. End language. Hint Resolve wff_SmartVarf wff_SmartVarVarf wff_SmartVarVarf_nil : wf. diff --git a/src/Reflection/WfReflective.v b/src/Reflection/WfReflective.v index d55b543cd..c54537fa2 100644 --- a/src/Reflection/WfReflective.v +++ b/src/Reflection/WfReflective.v @@ -156,7 +156,7 @@ Section language. -> @wff base_type_code op var1 var2 G t2 (eq_rect _ exprf (unnatize_exprf (List.length G) e1) _ p) (unnatize_exprf (List.length G) e2) | None => True end. - Proof. + Proof using base_type_eq_semidec_is_dec op_beq_bl. cbv zeta. destruct e1 as [ | | ? ? ? args | tx ex tC eC | ? ex ? ey ], e2 as [ | | ? ? ? args' | tx' ex' tC' eC' | ? ex' ? ey' ]; simpl; @@ -192,7 +192,7 @@ Section language. -> @wf base_type_code op var1 var2 t2 (eq_rect _ expr (unnatize_expr 0 e1) _ p) (unnatize_expr 0 e2) | None => True end. - Proof. + Proof using base_type_eq_semidec_is_dec op_beq_bl. destruct e1 as [ tx tR f ], e2 as [ tx' tR' f' ]; simpl; try solve [ exact I ]. pose proof (fun x x' @@ -223,7 +223,7 @@ Section Wf. : (forall var1 var2, to_prop (@reflect_wfT base_type_code base_type_eq_semidec_transparent op op_beq var1 var2 nil t t (e _) (e _))) -> Wf (fun var => unnatize_expr 0 (e (fun t => (nat * var t)%type))). - Proof. + Proof using base_type_eq_semidec_is_dec op_beq_bl. intros H var1 var2; specialize (H var1 var2). pose proof (@reflect_wf base_type_code base_type_eq_semidec_transparent base_type_eq_semidec_is_dec op op_beq op_beq_bl var1 var2 t t (e _) (e _)) as H'. rewrite type_eq_semidec_transparent_refl in H' by assumption; simpl in *. @@ -237,7 +237,7 @@ Section Wf. unnatize_expr 0 (e (fun t => (nat * var1 t)%type)) = e _ /\ to_prop (@reflect_wfT base_type_code base_type_eq_semidec_transparent op op_beq var1 var2 nil t t (e _) (e _))) -> Wf e. - Proof. + Proof using base_type_eq_semidec_is_dec op_beq_bl. intros H var1 var2. rewrite <- (proj1 (H var1 var2)), <- (proj1 (H var2 var2)). apply reflect_Wf_unnatize, H. diff --git a/src/Reflection/WfReflectiveGen.v b/src/Reflection/WfReflectiveGen.v index 0e484998b..23cdd8691 100644 --- a/src/Reflection/WfReflectiveGen.v +++ b/src/Reflection/WfReflectiveGen.v @@ -119,21 +119,21 @@ Section language. end end. Lemma base_type_eq_semidec_transparent_refl t : base_type_eq_semidec_transparent t t = Some eq_refl. - Proof. + Proof using base_type_eq_semidec_is_dec. clear -base_type_eq_semidec_is_dec. pose proof (base_type_eq_semidec_is_dec t t). destruct (base_type_eq_semidec_transparent t t); intros; try intuition congruence. inversion_base_type_code; reflexivity. Qed. Lemma flat_type_eq_semidec_transparent_refl t : flat_type_eq_semidec_transparent t t = Some eq_refl. - Proof. + Proof using base_type_eq_semidec_is_dec. clear -base_type_eq_semidec_is_dec. induction t as [t | | A B IHt]; simpl; try reflexivity. { rewrite base_type_eq_semidec_transparent_refl; reflexivity. } { rewrite_hyp !*; reflexivity. } Qed. Lemma type_eq_semidec_transparent_refl t : type_eq_semidec_transparent t t = Some eq_refl. - Proof. + Proof using base_type_eq_semidec_is_dec. clear -base_type_eq_semidec_is_dec. destruct t; simpl; rewrite !flat_type_eq_semidec_transparent_refl; reflexivity. Qed. @@ -189,13 +189,13 @@ Section language. Lemma duplicate_type_app ls ls' : (duplicate_type (ls ++ ls') = duplicate_type ls ++ duplicate_type ls')%list. - Proof. apply List.map_app. Qed. + Proof using Type. apply List.map_app. Qed. Lemma duplicate_type_length ls : List.length (duplicate_type ls) = List.length ls. - Proof. apply List.map_length. Qed. + Proof using Type. apply List.map_length. Qed. Lemma duplicate_type_in t v ls : List.In (existT _ (t, t) v) (duplicate_type ls) -> List.In (existT _ t v) ls. - Proof. + Proof using base_type_eq_semidec_is_dec. unfold duplicate_type; rewrite List.in_map_iff. intros [ [? ?] [? ?] ]. inversion_sigma; inversion_prod; inversion_base_type_code; subst; simpl. @@ -203,7 +203,7 @@ Section language. Qed. Lemma duplicate_type_not_in G t t0 v (H : base_type_eq_semidec_transparent t t0 = None) : ~List.In (existT _ (t, t0) v) (duplicate_type G). - Proof. + Proof using base_type_eq_semidec_is_dec. apply base_type_eq_semidec_is_dec in H. clear -H; intro H'. induction G as [|? ? IHG]; simpl in *; destruct H'; @@ -237,14 +237,14 @@ Section language. Arguments natize_interp_flat_type {var t} _ _. Lemma length_natize_interp_flat_type1 {t} (base : nat) (v1 : interp_flat_type var1 t) (v2 : interp_flat_type var2 t) : fst (natize_interp_flat_type base v1) = length (flatten_binding_list v1 v2) + base. - Proof. + Proof using Type. revert base; induction t; simpl; [ reflexivity | reflexivity | ]. intros; rewrite List.app_length, <- plus_assoc. rewrite_hyp <- ?*; reflexivity. Qed. Lemma length_natize_interp_flat_type2 {t} (base : nat) (v1 : interp_flat_type var1 t) (v2 : interp_flat_type var2 t) : fst (natize_interp_flat_type base v2) = length (flatten_binding_list v1 v2) + base. - Proof. + Proof using Type. revert base; induction t; simpl; [ reflexivity | reflexivity | ]. intros; rewrite List.app_length, <- plus_assoc. rewrite_hyp <- ?*; reflexivity. diff --git a/src/Reflection/Z/MapCastByDeBruijnInterp.v b/src/Reflection/Z/MapCastByDeBruijnInterp.v index 072563680..6e57136ab 100644 --- a/src/Reflection/Z/MapCastByDeBruijnInterp.v +++ b/src/Reflection/Z/MapCastByDeBruijnInterp.v @@ -44,7 +44,7 @@ Section language. Interp interp_op_bounds e input_bounds = b /\ @inbounds _ b (Interp interp_op e v) /\ cast_back _ _ (Interp interp_op e' v') = (Interp interp_op e v). - Proof. + Proof using Type*. apply MapCastCorrect; auto using internal_base_type_dec_lb. Qed. End language. |