blob: f3566d5c24cf78c0941071e7b0bb36baed19594e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
|
(* Declare Scope option_monad_scope. *)
Notation "'SOME' X <- A 'IN' B" := (match A with Some X => B | None => None end)
(at level 200, X ident, A at level 100, B at level 200)
: option_monad_scope.
Notation "'ASSERT' A 'IN' B" := (if A then B else None)
(at level 200, A at level 100, B at level 200)
: option_monad_scope.
Local Open Scope option_monad_scope.
(** Simple tactics for option-monad *)
Ltac deepest_match exp :=
match exp with
| context f [match ?expr with | _ => _ end] => ltac: (deepest_match expr)
| _ => exp
end.
Ltac autodestruct :=
let EQ := fresh "EQ" in
match goal with
| |- context f [match ?expr with | _ => _ end] =>
let t := ltac: (deepest_match expr) in
destruct t eqn:EQ; generalize EQ; clear EQ; congruence || trivial
end.
(* deprecated version of "autodestruct". the new one seems a better replacement
Ltac dummy_autodestruct :=
let EQ := fresh "EQ" in
match goal with
| |- context f [match ?expr with | _ => _ end] => destruct expr eqn:EQ; generalize EQ; clear EQ; congruence || trivial
end.
*)
Lemma destruct_SOME A B (P: option B -> Prop) (e: option A) (f: A -> option B):
(forall x, e = Some x -> P (f x)) -> (e = None -> P None) -> (P (SOME x <- e IN f x)).
Proof.
intros; destruct e; simpl; auto.
Qed.
Lemma destruct_ASSERT B (P: option B -> Prop) (e: bool) (x: option B):
(e = true -> P x) -> (e = false -> P None) -> (P (ASSERT e IN x)).
Proof.
intros; destruct e; simpl; auto.
Qed.
Ltac inversion_SOME x :=
try (eapply destruct_SOME; [ let x := fresh x in intro x | simpl; try congruence ]).
Ltac inversion_ASSERT :=
try (eapply destruct_ASSERT; [ idtac | simpl; try congruence ]).
Ltac simplify_someHyp :=
match goal with
| H: None = Some _ |- _ => inversion H; clear H; subst
| H: Some _ = None |- _ => inversion H; clear H; subst
| H: ?t = ?t |- _ => clear H
| H: Some _ = Some _ |- _ => inversion H; clear H; subst
| H: Some _ <> None |- _ => clear H
| H: None <> Some _ |- _ => clear H
| H: _ = Some _ |- _ => (try rewrite !H in * |- *); generalize H; clear H
| H: _ = None |- _ => (try rewrite !H in * |- *); generalize H; clear H
| H: None = _ |- _ => (try rewrite <- !H in * |- *); generalize H; clear H
end.
Ltac simplify_someHyps :=
repeat (simplify_someHyp; simpl in * |- *).
Ltac try_simplify_someHyps :=
try (intros; simplify_someHyps; eauto).
Ltac simplify_option := repeat (try_simplify_someHyps; autodestruct); try_simplify_someHyps.
|
