diff options
author | Jason Gross <jgross@mit.edu> | 2016-12-03 15:57:32 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-12-03 15:57:32 -0500 |
commit | 55c1a739ba0d254f50b30cf51fd007961be60b55 (patch) | |
tree | 6071c507c3d40cd4bfee7b10e6c9459049d6b557 | |
parent | 83fb85c8da71ed01e052b1be711c6090e5627f86 (diff) |
More powerful inversion_option
-rw-r--r-- | src/Reflection/ExprInversion.v | 13 | ||||
-rw-r--r-- | src/Util/Option.v | 40 |
2 files changed, 46 insertions, 7 deletions
diff --git a/src/Reflection/ExprInversion.v b/src/Reflection/ExprInversion.v index ecffbad97..2c2533454 100644 --- a/src/Reflection/ExprInversion.v +++ b/src/Reflection/ExprInversion.v @@ -52,7 +52,8 @@ Section language. repeat first [ intro | progress simpl in * | reflexivity - | tauto + | assumption + | progress destruct_head False | progress subst | progress inversion_option | progress inversion_sigma @@ -70,23 +71,23 @@ Section language. Lemma invert_Const_Some {t e v} : @invert_Const t e = Some v -> e = Const v. - Proof. t. Qed. + Proof. t. Defined. Lemma invert_Var_Some {t e v} : @invert_Var t e = Some v -> e = Var v. - Proof. t. Qed. + Proof. t. Defined. Lemma invert_Op_Some {t e v} : @invert_Op t e = Some v -> e = Op (fst (projT2 v)) (snd (projT2 v)). - Proof. t. Qed. + Proof. t. Defined. Lemma invert_LetIn_Some {t e v} : @invert_LetIn t e = Some v -> e = LetIn (fst (projT2 v)) (snd (projT2 v)). - Proof. t. Qed. + Proof. t. Defined. Lemma invert_Pair_Some {A B e v} : @invert_Pair A B e = Some v -> e = Pair (fst v) (snd v). - Proof. t. Qed. + Proof. t. Defined. End language. Global Arguments invert_Const {_ _ _ _ _} _. diff --git a/src/Util/Option.v b/src/Util/Option.v index 82ddf6750..64bdb4197 100644 --- a/src/Util/Option.v +++ b/src/Util/Option.v @@ -109,14 +109,52 @@ Ltac simpl_option_rect := (* deal with [option_rect _ _ _ None] and [option_rect end. Definition option_leq_to_eq {A} (x y : option A) : x = y -> option_eq eq x y. -Proof. destruct x; intro; subst; simpl; reflexivity. Qed. +Proof. destruct x; intro; subst; simpl; reflexivity. Defined. + +Definition option_eq_to_leq {A} (x y : option A) : option_eq eq x y -> x = y. +Proof. + destruct x, y; simpl; + try solve [ intros [] + | apply f_equal + | reflexivity + | apply eq_sym ]. +Defined. + +Lemma option_leq_to_eq_to_leq {A x y} v : @option_eq_to_leq A x y (@option_leq_to_eq A x y v) = v. +Proof. + destruct x; subst; simpl; reflexivity. +Qed. + +Lemma option_eq_to_leq_to_eq {A x y} v : @option_leq_to_eq A x y (@option_eq_to_leq A x y v) = v. +Proof. + compute in *. + repeat first [ progress subst + | progress break_match + | reflexivity ]. +Qed. + +Lemma UIP_None {A} (p q : @None A = @None A) : p = q. +Proof. + rewrite <- (option_leq_to_eq_to_leq p), <- (option_leq_to_eq_to_leq q); simpl; reflexivity. +Qed. + +Lemma invert_eq_Some {A x y} (p : Some x = Some y) : { pf : x = y | @option_eq_to_leq A (Some x) (Some y) pf = p }. +Proof. + eexists; apply option_leq_to_eq_to_leq. +Qed. Ltac inversion_option_step := match goal with | [ H : Some _ = Some _ |- _ ] => apply option_leq_to_eq in H; unfold option_eq in H + | [ H : Some _ = Some _ |- _ ] + => let H' := fresh in + rename H into H'; + destruct (invert_eq_Some H') as [H ?]; subst H' | [ H : None = Some _ |- _ ] => solve [ inversion H ] | [ H : Some _ = None |- _ ] => solve [ inversion H ] | [ H : None = None |- _ ] => clear H + | [ H : None = None |- _ ] + => assert (eq_refl = H) by apply UIP_None; subst H end. Ltac inversion_option := repeat inversion_option_step. |