forked from coq/coq
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Support module substitution of rewrite strategies. Fixes coq#18463
- Loading branch information
1 parent
4fcf594
commit a8b39cb
Showing
7 changed files
with
60 additions
and
11 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
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,38 @@ | ||
From Coq Require Import Setoid. | ||
|
||
Module Type Nop. End Nop. | ||
Module nop. End nop. | ||
|
||
Module RewriteStratSubstTestF (Nop : Nop). | ||
Axiom X : Set. | ||
|
||
Axiom f : X -> X. | ||
Axiom g : X -> X -> X. | ||
Axiom h : nat -> X -> X. | ||
|
||
Axiom lem0 : forall x, f (f x) = f x. | ||
Axiom lem1 : forall x, g x x = f x. | ||
Axiom lem2 : forall n x, h (S n) x = g (h n x) (h n x). | ||
Axiom lem3 : forall x, h 0 x = x. | ||
Definition idnat := @id nat. | ||
|
||
Ltac rs1 := rewrite_strat topdown lem2. | ||
Ltac rs2 := rewrite_strat try fold idnat. | ||
Ltac rs3 := rewrite_strat try subterms lem2. | ||
Ltac rs4 := rewrite_strat eval cbv delta [idnat]. | ||
End RewriteStratSubstTestF. | ||
|
||
Module RewriteStratSubstTest := RewriteStratSubstTestF nop. | ||
|
||
Goal forall x, RewriteStratSubstTest.h 6 x = RewriteStratSubstTest.f x /\ RewriteStratSubstTest.idnat 5 = id 5. | ||
intros. | ||
Print Ltac RewriteStratSubstTest.rs1. (* Ltac RewriteStratSubstTest.rs1 := Coq.Init.Ltac.rewrite_strat_#_521927FC _ (* Generic printer *) *) | ||
RewriteStratSubstTest.rs1. (* Error: Anomaly "Constant rewrite_strat.RewriteStratSubstTestF.lem2 does not appear in the environment." | ||
Please report at http://coq.inria.fr/bugs/. *) | ||
Undo 1. | ||
RewriteStratSubstTest.rs2. | ||
Undo 1. | ||
RewriteStratSubstTest.rs3. | ||
Undo 1. | ||
RewriteStratSubstTest.rs4. | ||
Admitted. |