blob: 92c7b51ad6dcef529236733aed3af89434efda96 (
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
|
Require Import Crypto.Util.FixCoqMistakes.
Require Import Coq.Classes.Morphisms Coq.Relations.Relation_Definitions.
Require Import Crypto.Util.Tactics.GetGoal.
Require Import Crypto.Util.Notations.
Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y.
Definition Let_In_pf {A P} (x : A) (f : forall a : A, a = x -> P a) : P x := let y := x in f y eq_refl.
Notation "'dlet_nd' x .. y := v 'in' f" := (Let_In (P:=fun _ => _) v (fun x => .. (fun y => f) .. )) (only parsing).
Notation "'dlet' x .. y := v 'in' f" := (Let_In v (fun x => .. (fun y => f) .. )).
Notation "'pflet' x , pf := y 'in' f" := (Let_In_pf y (fun x pf => f)).
Module Bug5107WorkAround.
Notation "'dlet' x .. y := v 'in' f" := (Let_In (P:=fun _ => _) v (fun x => .. (fun y => f) .. )).
End Bug5107WorkAround.
Global Instance Proper_Let_In_nd_changebody {A P R} {Reflexive_R:@Reflexive P R}
: Proper (eq ==> pointwise_relation _ R ==> R) (@Let_In A (fun _ => P)).
Proof. lazy; intros; subst; auto; congruence. Qed.
Global Instance Proper_Let_In_nd_changevalue {A B} (RA:relation A) {RB:relation B}
: Proper (RA ==> (RA ==> RB) ==> RB) (Let_In (P:=fun _=>B)).
Proof. cbv; intuition. Qed.
Lemma Proper_Let_In_nd_changebody_eq {A P R} {Reflexive_R:@Reflexive P R} {x}
: Proper ((fun f g => forall a, x = a -> R (f a) (g a)) ==> R) (@Let_In A (fun _ => P) x).
Proof. lazy; intros; subst; auto; congruence. Qed.
Definition app_Let_In_nd {A B T} (f:B->T) (e:A) (C:A->B)
: f (Let_In e C) = Let_In e (fun v => f (C v)) := eq_refl.
Definition Let_app_In_nd {A B T} (f:A->B) (e:A) (C:B->T)
: Let_In (f e) C = Let_In e (fun v => C (f v)) := eq_refl.
Class _call_let_in_to_Let_In {T} (e:T) := _let_in_to_Let_In_return : T.
(* : forall T, gallina T -> gallina T, structurally recursive in the argument *)
Ltac let_in_to_Let_In e :=
lazymatch e with
| let x := ?ex in @?eC x =>
let ex := let_in_to_Let_In ex in
let eC := let_in_to_Let_In eC in
constr:(Let_In ex eC)
| ?f ?x =>
let f := let_in_to_Let_In f in
let x := let_in_to_Let_In x in
constr:(f x)
| (fun x : ?T => ?C) =>
lazymatch constr:(fun (x : T) => (_ : _call_let_in_to_Let_In C))
(* [C] here above is an open term that references "x" by name *)
with fun x => @?C x => C end (* match drops the type cast *)
| ?x => x
end.
Hint Extern 0 (_call_let_in_to_Let_In ?e) => (
let e := let_in_to_Let_In e in eexact e
) : typeclass_instances.
Ltac change_let_in_with_Let_In :=
let g := get_goal in
let g' := let_in_to_Let_In g in
change g'.
|
