blob: 54d79ee486db843c375cbace144a435e3b9174fb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
Ltac simplify_repeated_ifs_step :=
match goal with
| [ |- context G[if ?b then ?x else ?y] ]
=> let x' := match x with
| context x'[b] => let x'' := context x'[true] in x''
end in
let G' := context G[if b then x' else y] in
cut G'; [ destruct b; exact (fun z => z) | cbv iota ]
| [ |- context G[if ?b then ?x else ?y] ]
=> let y' := match y with
| context y'[b] => let y'' := context y'[false] in y''
end in
let G' := context G[if b then x else y'] in
cut G'; [ destruct b; exact (fun z => z) | cbv iota ]
end.
Ltac simplify_repeated_ifs := repeat simplify_repeated_ifs_step.
|
