diff options
author | 2018-07-26 17:57:21 -0400 | |
---|---|---|
committer | 2018-07-26 17:57:21 -0400 | |
commit | 055aff88a4d6c67f333735801ceac583c3761ba9 (patch) | |
tree | 2ec87aca8f231b5a07390e58f46b475243a1981f /src | |
parent | 3be09bcbc00ce64fae429f7e2e663c5a7d400dfa (diff) |
Minor improvements to wf framework
Diffstat (limited to 'src')
-rw-r--r-- | src/Experiments/NewPipeline/LanguageInversion.v | 194 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/LanguageWf.v | 9 |
2 files changed, 113 insertions, 90 deletions
diff --git a/src/Experiments/NewPipeline/LanguageInversion.v b/src/Experiments/NewPipeline/LanguageInversion.v index 9b4dd8ff1..e65630e43 100644 --- a/src/Experiments/NewPipeline/LanguageInversion.v +++ b/src/Experiments/NewPipeline/LanguageInversion.v @@ -12,6 +12,76 @@ Require Import Crypto.Util.FixCoqMistakes. Import EqNotations. Module Compilers. Import Language.Compilers. + + Module base. + Module type. + Section encode_decode. + Definition code (t1 t2 : base.type) : Prop + := match t1, t2 with + | base.type.type_base t1, base.type.type_base t2 => t1 = t2 + | base.type.prod A1 B1, base.type.prod A2 B2 => A1 = A2 /\ B1 = B2 + | base.type.list A1, base.type.list A2 => A1 = A2 + | base.type.type_base _, _ + | base.type.prod _ _, _ + | base.type.list _, _ + => False + end. + + Definition encode (x y : base.type) : x = y -> code x y. + Proof. intro p; destruct p, x; repeat constructor. Defined. + Definition decode (x y : base.type) : code x y -> x = y. + Proof. destruct x, y; intro p; try assumption; destruct p; (apply f_equal || apply f_equal2); (assumption || reflexivity). Defined. + + Definition path_rect {x y : base.type} (Q : x = y -> Type) + (f : forall p, Q (decode x y p)) + : forall p, Q p. + Proof. intro p; specialize (f (encode x y p)); destruct x, p; exact f. Defined. + End encode_decode. + + Global Instance base_eq_Decidable : DecidableRel (@eq base.type.base) := base.type.base_eq_dec. + Global Instance base_type_eq_Decidable : DecidableRel (@eq base.type.type) := base.type.type_eq_dec. + Global Instance base_eq_HProp : IsHPropRel (@eq base.type.base) := _. + Global Instance base_type_eq_HProp : IsHPropRel (@eq base.type.type) := _. + + Ltac induction_type_in_using H rect := + induction H as [H] using (rect _ _); + cbv [code] in H; + let H1 := fresh H in + let H2 := fresh H in + try lazymatch type of H with + | False => exfalso; exact H + | True => destruct H + | ?x = ?x => clear H + | _ = _ :> base.type.base => try solve [ exfalso; inversion H ] + | _ /\ _ => destruct H as [H1 H2] + end. + + Ltac inversion_type_step := + cbv [defaults.type_base] in *; + first [ lazymatch goal with + | [ H : ?x = ?x :> base.type.type |- _ ] => clear H || eliminate_hprop_eq_helper H base_type_eq_HProp + | [ H : ?x = ?x :> base.type.base |- _ ] => clear H || eliminate_hprop_eq_helper H base_eq_HProp + | [ H : ?x = ?y :> base.type.type |- _ ] => subst x || subst y + | [ H : ?x = ?y :> base.type.base |- _ ] => subst x || subst y + end + | lazymatch goal with + | [ H : _ = base.type.type_base _ |- _ ] + => induction_type_in_using H @path_rect + | [ H : base.type.type_base _ = _ |- _ ] + => induction_type_in_using H @path_rect + | [ H : _ = base.type.prod _ _ |- _ ] + => induction_type_in_using H @path_rect + | [ H : base.type.prod _ _ = _ |- _ ] + => induction_type_in_using H @path_rect + | [ H : _ = base.type.list _ |- _ ] + => induction_type_in_using H @path_rect + | [ H : base.type.list _ = _ |- _ ] + => induction_type_in_using H @path_rect + end ]. + Ltac inversion_type := repeat inversion_type_step. + End type. + End base. + Module type. Section with_base. Context {base_type : Type}. @@ -81,76 +151,15 @@ Module Compilers. => refine (@preinvert_one_type _ P t Q _) end; intros ? e ?; intros; cbv [mark]. - End type. - Module base. - Module type. - Section encode_decode. - Definition code (t1 t2 : base.type) : Prop - := match t1, t2 with - | base.type.type_base t1, base.type.type_base t2 => t1 = t2 - | base.type.prod A1 B1, base.type.prod A2 B2 => A1 = A2 /\ B1 = B2 - | base.type.list A1, base.type.list A2 => A1 = A2 - | base.type.type_base _, _ - | base.type.prod _ _, _ - | base.type.list _, _ - => False - end. - - Definition encode (x y : base.type) : x = y -> code x y. - Proof. intro p; destruct p, x; repeat constructor. Defined. - Definition decode (x y : base.type) : code x y -> x = y. - Proof. destruct x, y; intro p; try assumption; destruct p; (apply f_equal || apply f_equal2); (assumption || reflexivity). Defined. - - Definition path_rect {x y : base.type} (Q : x = y -> Type) - (f : forall p, Q (decode x y p)) - : forall p, Q p. - Proof. intro p; specialize (f (encode x y p)); destruct x, p; exact f. Defined. - End encode_decode. - - Global Instance base_eq_Decidable : DecidableRel (@eq base.type.base) := base.type.base_eq_dec. - Global Instance base_type_eq_Decidable : DecidableRel (@eq base.type.type) := base.type.type_eq_dec. - Global Instance base_eq_HProp : IsHPropRel (@eq base.type.base) := _. - Global Instance base_type_eq_HProp : IsHPropRel (@eq base.type.type) := _. - - Ltac induction_type_in_using H rect := - induction H as [H] using (rect _ _); - cbv [code] in H; - let H1 := fresh H in - let H2 := fresh H in - try lazymatch type of H with - | False => exfalso; exact H - | True => destruct H - | ?x = ?x => clear H - | _ = _ :> base.type.base => try solve [ exfalso; inversion H ] - | _ /\ _ => destruct H as [H1 H2] - end. - - Ltac inversion_type_step := - cbv [defaults.type_base] in *; - first [ lazymatch goal with - | [ H : ?x = ?x :> base.type.type |- _ ] => clear H || eliminate_hprop_eq_helper H base_type_eq_HProp - | [ H : ?x = ?x :> base.type.base |- _ ] => clear H || eliminate_hprop_eq_helper H base_eq_HProp - | [ H : ?x = ?y :> base.type.type |- _ ] => subst x || subst y - | [ H : ?x = ?y :> base.type.base |- _ ] => subst x || subst y - end - | lazymatch goal with - | [ H : _ = base.type.type_base _ |- _ ] - => induction_type_in_using H @path_rect - | [ H : base.type.type_base _ = _ |- _ ] - => induction_type_in_using H @path_rect - | [ H : _ = base.type.prod _ _ |- _ ] - => induction_type_in_using H @path_rect - | [ H : base.type.prod _ _ = _ |- _ ] - => induction_type_in_using H @path_rect - | [ H : _ = base.type.list _ |- _ ] - => induction_type_in_using H @path_rect - | [ H : base.type.list _ = _ |- _ ] - => induction_type_in_using H @path_rect - end ]. - Ltac inversion_type := repeat inversion_type_step. - End type. - End base. + Ltac invert_one e := + generalize_one_eq_var e; + destruct e; + try discriminate; + type.inversion_type; + base.type.inversion_type; + cbn [type.decode base.type.decode f_equal f_equal2 eq_rect] in *. + End type. Module expr. Section with_var. @@ -222,34 +231,21 @@ Module Compilers. End encode_decode. End with_var. - Ltac invert_one e := - type.generalize_one_eq_var e; - destruct e; - try discriminate; - type.inversion_type; - base.type.inversion_type; - cbn [type.decode base.type.decode f_equal f_equal2 eq_rect] in *. - Ltac invert_step := match goal with - | [ e : expr (type.base _) |- _ ] => invert_one e - | [ e : expr (type.arrow _ _) |- _ ] => invert_one e + | [ e : expr.expr (type.base _) |- _ ] => type.invert_one e + | [ e : expr.expr (defaults.type_base _) |- _ ] => type.invert_one e + | [ e : expr.expr (type.arrow _ _) |- _ ] => type.invert_one e end. Ltac invert := repeat invert_step. Ltac invert_match_step := match goal with - | [ |- context[match ?e with expr.Ident _ _ => _ | _ => _ end] ] - => invert_one e - | [ |- context[match ?e with expr.Var _ _ => _ end] ] - => invert_one e - | [ |- context[match ?e with expr.App _ _ _ _ => _ end] ] - => invert_one e - | [ |- context[match ?e with expr.LetIn _ _ _ _ => _ end] ] - => invert_one e - | [ |- context[match ?e with expr.Abs _ _ _ => _ end] ] - => invert_one e + | [ H : context[match ?e with expr.Var _ _ => _ | _ => _ end] |- _ ] + => type.invert_one e + | [ |- context[match ?e with expr.Var _ _ => _ | _ => _ end] ] + => type.invert_one e end. Ltac invert_match := repeat invert_match_step. @@ -308,4 +304,24 @@ Module Compilers. end. Ltac inversion_expr := repeat inversion_expr_step. End expr. + + Module ident. + Ltac invert_step := + match goal with + | [ e : ident (type.base _) |- _ ] => type.invert_one e + | [ e : ident (type.arrow _ _) |- _ ] => type.invert_one e + end. + + Ltac invert := repeat invert_step. + + Ltac invert_match_step := + match goal with + | [ H : context[match ?e with ident.Literal _ _ => _ | _ => _ end] |- _ ] + => type.invert_one e + | [ |- context[match ?e with ident.Literal _ _ => _ | _ => _ end] ] + => type.invert_one e + end. + + Ltac invert_match := repeat invert_match_step. + End ident. End Compilers. diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v index 5e9696d77..2aac184ec 100644 --- a/src/Experiments/NewPipeline/LanguageWf.v +++ b/src/Experiments/NewPipeline/LanguageWf.v @@ -585,8 +585,15 @@ Module Compilers. | [ H : context[expr.interp _ _ == expr.interp _ _] |- expr.interp _ _ == expr.interp _ _ ] => eapply H; eauto with nocore; solve [ repeat interp_safe_t_step ] end ]. + Ltac interp_unsafe_t_step := + first [ solve [ eauto with nocore ] + | match goal with + | [ H : context[expr.interp _ _ == expr.interp _ _] |- expr.interp _ _ == expr.interp _ _ ] + => eapply H; eauto with nocore; match goal with |- ?G => tryif has_evar G then fail else idtac end + end ]. Ltac interp_safe_t := repeat interp_safe_t_step. - Ltac interp_t_step := first [ interp_safe_t_step ]. + Ltac interp_unsafe_t := repeat interp_unsafe_t_step. + Ltac interp_t_step := first [ interp_safe_t_step | interp_unsafe_t_step ]. Ltac interp_t := repeat interp_t_step. |