-
Notifications
You must be signed in to change notification settings - Fork 23
/
destr.v
26 lines (23 loc) · 1002 Bytes
/
destr.v
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
(* adds BoolSpec instances needed to destruct booleans into Props *)
Require Import coqutil.Decidable.
Ltac subst_after_destr_default H :=
match type of H with
| ?x = ?y =>
(* subst picks the first suitable equality from the top, so we move H at top *)
move H at top; (subst x || subst y)
| _ => idtac
end.
(* `Ltac subst_after_destr H ::= idtac.` disables substitution of equalities found by destr *)
Ltac subst_after_destr H := subst_after_destr_default H.
Ltac destr d :=
match type of d with
| _ => is_var d; destruct d
| sumbool _ _ => destruct d
| bool =>
let B := fresh "B" in eassert (BoolSpec _ _ d) as B by typeclasses eauto;
let tB := type of B in
tryif constr_eq tB (BoolSpec (d = true) (d = false) d)
then fail (* only the default BoolSpec was found, which is not interesting to us *)
else (let E := fresh "E" in destruct B as [E|E]; subst_after_destr E)
| _ => let E := fresh "E" in destruct d eqn: E; subst_after_destr E
end.