blob: e6fc3055b255fed408b29968476b4f985ea5edaa (
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
|
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.TypeInversion.
Require Import Crypto.Compilers.Z.Syntax.
Ltac invert_one_op e :=
preinvert_one_type e;
intros ? e;
destruct e;
try exact I.
Ltac invert_op_step :=
match goal with
| [ e : op _ (Tbase _) |- _ ] => invert_one_op e
| [ e : op _ (Prod _ _) |- _ ] => invert_one_op e
| [ e : op _ Unit |- _ ] => invert_one_op e
end.
Ltac invert_op := repeat invert_op_step.
Ltac invert_match_op_step :=
match goal with
| [ |- context[match ?e with OpConst _ _ => _ | _ => _ end] ]
=> invert_one_op e
| [ H : context[match ?e with OpConst _ _ => _ | _ => _ end] |- _ ]
=> invert_one_op e
end.
Ltac invert_match_op := repeat invert_match_op_step.
|
