blob: 984d2a3e18171eff658a8839fda1180397081c53 (
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
|
Require Import Crypto.Compilers.Named.PositiveContext.
Require Import Crypto.Compilers.Named.InterpretToPHOASWf.
Require Import Crypto.Compilers.Named.CompileWf.
Require Import Crypto.Compilers.Named.WfFromUnit.
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.Wf.
Require Import Crypto.Compilers.Z.Syntax.
Require Import Crypto.Compilers.Z.RewriteAddToAdc.
Require Import Crypto.Util.Tactics.BreakMatch.
Require Import Crypto.Util.Decidable.
Require Import Crypto.Util.Bool.
Section language.
Local Hint Resolve internal_base_type_dec_lb internal_base_type_dec_lb dec_rel_of_bool_dec_rel : typeclass_instances.
Lemma Wf_RewriteAdc {t} (e : Expr t) (Hwf : Wf e)
: Wf (RewriteAdc e).
Proof.
unfold RewriteAdc, option_map; break_innermost_match;
[ .. | solve [ intros var1 var2; destruct (Hwf var1 var2); auto with wf ] ];
repeat first [ eapply @Wf_InterpToPHOAS with (t:=Arrow _ _)
| progress split_andb
| congruence
| intros;
match goal with
| [ |- ContextDefinitions.ContextOk _ ]
=> eapply @PositiveContextOk
end
| solve [ auto | eapply @BinPos.Pos.eqb_eq ]
| eapply @Wf_from_unit
| eapply @dec_rel_of_bool_dec_rel
| eapply @internal_base_type_dec_lb
| eapply @internal_base_type_dec_bl
| intros var1 var2; specialize (Hwf var1 var2); destruct Hwf;
constructor; assumption ].
Qed.
End language.
Hint Resolve Wf_RewriteAdc : wf.
|
