-
Notifications
You must be signed in to change notification settings - Fork 147
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add some util lemmas and definitions
- Loading branch information
1 parent
78b499b
commit 8c6b7c9
Showing
10 changed files
with
225 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
Require Export Crypto.Util.Notations. | ||
|
||
Ltac beta1 x := | ||
lazymatch x with | ||
| (fun a => ?f) ?b => constr:(subst_let a := b in f) | ||
end. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,4 @@ | ||
Require Export Crypto.Util.FixCoqMistakes. | ||
|
||
Ltac delta1 x := | ||
eval cbv delta [x] in x. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
Require Export Crypto.Util.FixCoqMistakes. | ||
Require Import Crypto.Util.Tactics.Zeta1. | ||
Require Import Coq.ssr.ssreflect. | ||
|
||
Ltac generalize_over_holes tac := | ||
zeta1 (ltac:(let H := fresh in | ||
(pose H := ltac:(let v := tac () in refine v)); | ||
exact H)). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,16 @@ | ||
Require Import Crypto.Util.Tactics.Head. | ||
|
||
Ltac head_constr_eq T1 T2 := | ||
let h1 := head T1 in | ||
let h2 := head T2 in | ||
constr_eq h1 h2. | ||
|
||
Ltac head_constr_eq_nounivs T1 T2 := | ||
let h1 := head T1 in | ||
let h2 := head T2 in | ||
constr_eq_nounivs h1 h2. | ||
|
||
Ltac head_constr_eq_strict T1 T2 := | ||
let h1 := head T1 in | ||
let h2 := head T2 in | ||
constr_eq_strict h1 h2. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,74 @@ | ||
Require Import Crypto.Util.Tactics.SpecializeBy. | ||
Require Import Crypto.Util.Tactics.GeneralizeOverHoles. | ||
|
||
Ltac guarded_specialize_term_under_binders_by' guard_tac H tac := | ||
lazymatch type of H with | ||
| forall a, _ | ||
=> match goal with | ||
| _ => let __ := lazymatch goal with _ => guard_tac H end in | ||
open_constr:(H ltac:(progress tac)) | ||
| _ => let H := open_constr:(H _) in | ||
guarded_specialize_term_under_binders_by' guard_tac H tac | ||
end | ||
end. | ||
|
||
Ltac guarded_specialize_term_under_binders_by guard_tac H tac := | ||
generalize_over_holes ltac:(fun _ => guarded_specialize_term_under_binders_by' guard_tac H tac). | ||
|
||
Ltac guarded_specialize_hyp_under_binders_by guard_tac H tac := | ||
idtac; | ||
let is_transparent := match goal with | ||
| _ => let __ := (eval cbv delta [H] in H) in | ||
constr:(true) | ||
| _ => constr:(false) | ||
end in | ||
lazymatch is_transparent with | ||
| true | ||
=> let H' := fresh in | ||
rename H into H'; | ||
let H'' := guarded_specialize_term_under_binders_by guard_tac H' tac in | ||
pose H'' as H; | ||
subst H' | ||
| false | ||
=> let H := guarded_specialize_term_under_binders_by guard_tac H tac in | ||
specialize H | ||
end. | ||
|
||
Ltac guard_noop H := idtac. | ||
|
||
Ltac guard_nondep H := | ||
lazymatch type of H with | ||
| ?A -> ?B => idtac | ||
end. | ||
|
||
(** try to specialize all non-dependent hypotheses using [tac] at any point under their binders, maintaining transparency *) | ||
Ltac guarded_specialize_under_binders_by' tac guard_tac := | ||
idtac; | ||
match goal with | ||
| [ H : _ |- _ ] | ||
=> guard_tac H; | ||
guarded_specialize_hyp_under_binders_by guard_nondep H tac | ||
end. | ||
Ltac guarded_specialize_dep_under_binders_by' tac guard_tac := | ||
idtac; | ||
match goal with | ||
| [ H : _ |- _ ] | ||
=> guard_tac H; | ||
guarded_specialize_hyp_under_binders_by guard_noop H tac | ||
end. | ||
|
||
Ltac specialize_under_binders_by' tac := guarded_specialize_under_binders_by' tac ltac:(fun _ => idtac). | ||
Ltac specialize_dep_under_binders_by' tac := guarded_specialize_dep_under_binders_by' tac ltac:(fun _ => idtac). | ||
|
||
Ltac guarded_specialize_under_binders_by tac guard_tac := repeat guarded_specialize_under_binders_by' tac guard_tac. | ||
Ltac guarded_specialize_dep_under_binders_by tac guard_tac := repeat guarded_specialize_dep_under_binders_by' tac guard_tac. | ||
|
||
Ltac specialize_under_binders_by tac := repeat specialize_under_binders_by' tac. | ||
Ltac specialize_dep_under_binders_by tac := repeat specialize_dep_under_binders_by' tac. | ||
|
||
(** [specialize_under_binders_by auto] should not mean [specialize_under_binders_by ( auto | ||
with * )]!!!!!!! (see | ||
https://coq.inria.fr/bugs/show_bug.cgi?id=4966) We fix this design | ||
flaw. *) | ||
Tactic Notation "specialize_under_binders_by" tactic3(tac) := specialize_under_binders_by tac. | ||
Tactic Notation "specialize_dep_under_binders_by" tactic3(tac) := specialize_dep_under_binders_by tac. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
Require Export Crypto.Util.Notations. | ||
|
||
Ltac zeta1 x := | ||
lazymatch x with | ||
| let a := ?b in ?f => constr:(subst_let a := b in f) | ||
end. |