diff options
author | Jason Gross <jgross@mit.edu> | 2017-10-03 01:33:42 -0400 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2017-10-18 23:01:29 -0400 |
commit | 239356d3a22af3b065dfae10bd6d84dd509251e8 (patch) | |
tree | 856190fd79b47d4eaf13384ff010c7dca04e10df | |
parent | 02a16ddc62000314543dcbfaf859448b0a42c7a1 (diff) |
Add 8.7-only CacheTerm
-rw-r--r-- | src/Util/Tactics/CacheTerm.v | 47 |
1 files changed, 47 insertions, 0 deletions
diff --git a/src/Util/Tactics/CacheTerm.v b/src/Util/Tactics/CacheTerm.v index 4313a7f02..7541f907e 100644 --- a/src/Util/Tactics/CacheTerm.v +++ b/src/Util/Tactics/CacheTerm.v @@ -12,8 +12,55 @@ Ltac cache_term_with_type_by_gen ty abstract_tac id := | _ => clear id' end in ret. +Ltac cache_term_with_type_by ty tac id := + cache_term_with_type_by_gen ty ltac:(fun id' => transparent_abstract tac using id') id. Ltac cache_proof_with_type_by ty tac id := cache_term_with_type_by_gen ty ltac:(fun id' => abstract tac using id') id. +Ltac cache_term_by tac id := + let ty := open_constr:(_) in + cache_term_with_type_by ty tac id. Ltac cache_proof_by ty tac id := let ty := open_constr:(_) in cache_proof_with_type_by ty tac id. +Ltac cache_term term id := + let ty := type of term in + cache_term_with_type_by ty ltac:(exact_no_check term) id. + +Ltac cache_sig_red_with_type_by ty tac red_tac red_cast_no_check id := + let id' := fresh id in + let id' := fresh id in + let id' := cache_term_with_type_by ty tac id' in + let P := lazymatch ty with sig ?P => P end in + cache_term_with_type_by + ty + ltac:(let v := (eval cbv beta iota delta [id' proj1_sig] in (proj1_sig id')) in + let v := red_tac v in + (exists v); + abstract ( + refine (eq_rect _ P (proj2_sig id') _ _); + red_cast_no_check (eq_refl v) + )) + id. +Ltac cache_sig_red_with_type ty term red_tac red_cast_no_check id := + let id' := fresh id in + let id' := fresh id in + let id' := cache_term term id' in + let P := lazymatch ty with sig ?P => P end in + cache_term_with_type_by + ty + ltac:(let v := (eval cbv beta iota delta [id' proj1_sig] in (proj1_sig id')) in + let v := red_tac v in + (exists v); + abstract ( + refine (eq_rect _ P (proj2_sig id') _ _); + red_cast_no_check (eq_refl v) + )) + id. +Ltac cache_sig_with_type_by ty tac id + := cache_sig_red_with_type_by ty tac ltac:(fun v => v) exact_no_check id. +Ltac cache_vm_sig_with_type_by ty tac id + := cache_sig_red_with_type_by ty tac ltac:(fun v => eval vm_compute in v) vm_cast_no_check id. +Ltac cache_sig_with_type ty term id + := cache_sig_red_with_type ty term ltac:(fun v => v) exact_no_check id. +Ltac cache_vm_sig_with_type ty term id + := cache_sig_red_with_type ty term ltac:(fun v => eval vm_compute in v) vm_cast_no_check id. |