File: bug_18463.v

package info (click to toggle)
coq 8.20.1%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: sid, trixie
  • size: 44,116 kB
  • sloc: ml: 234,160; sh: 4,301; python: 3,270; ansic: 2,644; makefile: 882; lisp: 172; javascript: 63; xml: 24; sed: 2
file content (38 lines) | stat: -rw-r--r-- 1,263 bytes parent folder | download | duplicates (2)
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
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.