blob: d5374e8cec03366ce5f318a27a82100553d9a2c2 (
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
|
Require Import Coq.ZArith.ZArith.
Require Import Crypto.Util.CPSNotations.
Require Import Crypto.Util.ZRange.
Require Import Crypto.Util.Tactics.BreakMatch.
Require Import Crypto.Util.Option.
Require Import Crypto.Experiments.NewPipeline.Language.
Require Import Crypto.Experiments.NewPipeline.GENERATEDIdentifiersWithoutTypes.
Import EqNotations.
Module Compilers.
Import Language.Compilers.
Import GENERATEDIdentifiersWithoutTypes.Compilers.
Module pattern.
Import GENERATEDIdentifiersWithoutTypes.Compilers.pattern.
Module ident.
Import GENERATEDIdentifiersWithoutTypes.Compilers.pattern.ident.
Local Lemma quick_invert_eq_option {A} (P : Type) (x y : option A) (H : x = y)
: match x, y return Type with
| Some _, None => P
| None, Some _ => P
| _, _ => True
end.
Proof. subst y; destruct x; constructor. Qed.
Lemma pident_to_typed_invert_bind_args_type__pident_to_typed_invert_bind_args t idc p f
: @invert_bind_args t idc p = Some f
-> { pf : t = type_of p f | @to_typed p f = rew [Compilers.ident.ident] pf in idc }.
Proof.
cbv [invert_bind_args type_of full_types].
repeat first [ reflexivity
| (exists eq_refl)
| progress intros
| match goal with
| [ H : Some _ = None |- ?P ] => exact (@quick_invert_eq_option _ P _ _ H)
| [ H : None = Some _ |- ?P ] => exact (@quick_invert_eq_option _ P _ _ H)
end
| progress inversion_option
| progress subst
| break_innermost_match_step
| break_innermost_match_hyps_step ].
Qed.
Lemma pident_to_typed_invert_bind_args_type t idc p f
: @invert_bind_args t idc p = Some f -> t = type_of p f.
Proof.
intro pf; exact (proj1_sig (@pident_to_typed_invert_bind_args_type__pident_to_typed_invert_bind_args t idc p f pf)).
Defined.
Lemma pident_to_typed_invert_bind_args t idc p f (pf : @invert_bind_args t idc p = Some f)
: @to_typed p f = rew [Compilers.ident.ident] @pident_to_typed_invert_bind_args_type t idc p f pf in idc.
Proof.
exact (proj2_sig (@pident_to_typed_invert_bind_args_type__pident_to_typed_invert_bind_args t idc p f pf)).
Defined.
Lemma try_make_transport_ident_cps_correct P idc1 idc2 T k
: try_make_transport_ident_cps P idc1 idc2 T k
= k (match Sumbool.sumbool_of_bool (ident_beq idc1 idc2) with
| left pf => Some (fun v => rew [P] internal_ident_dec_bl _ _ pf in v)
| right _ => None
end).
Proof.
destruct (Sumbool.sumbool_of_bool (ident_beq idc1 idc2)) as [pf|pf].
{ generalize (internal_ident_dec_bl idc1 idc2 pf); clear pf; intro; subst idc2; cbn [eq_rect].
destruct idc1; reflexivity. }
{ destruct idc1, idc2; try reflexivity; solve [ inversion pf ]. }
Qed.
End ident.
End pattern.
End Compilers.
|
