The Coq mailing list

[Fabian Kunze <s9fakunz AT stud.uni-saarland.de>]

Hello,

I'm currently writing tactics for an call-by-value Lambda calculus (in
coq 8.5beta2).

II have rules for autorewrite with constrains. But those constrains can
only be satisfied when using an depth-first rewriting. (For more
details: See the 'minimal' example at the end of the mail).

So I think that either I need an depth-first autorewrite or an way to
tell auto 'if the tactic solving the constrains fails, try rewriting
at the next position'.

I heard that there is some undocumented, new feature in autorewrite
that could possibly help me, so does enyone know of this?

Best,
Fabian

Appendix: complete code

Require Import Morphisms Relation_Definitions Setoid.

Axiom V : Type.

Inductive Term :=
| application : Term -> Term -> Term
| value : V -> Term.

Inductive isVal : Term -> Prop :=
| valueC x : isVal (value x).

Axiom reduces : Term -> Term -> Prop.

(* fancy notation that allows us to just write "F x" instead of
application (value F) (value x) *)
Coercion application : Term >-> Funclass.
Coercion value : V >-> Term.


Notation "s >> t" := (reduces s t) (at level 50).

(* register Term as an reasonable rewrite system *)
Instance red_PreOrder : PreOrder reduces. Admitted.
Instance red_app_proper : Proper (reduces ==> reduces ==> reduces)
application. Admitted.

Variable K : Term.
Axiom K_red: forall s t : Term, isVal s -> isVal t -> K s t >> s.

(* I can prove this by hand: *)
Lemma testmanual s t u: isVal s -> isVal t -> isVal u -> K (K s t) u >> s.
Proof with try assumption.
  intros. setoid_rewrite K_red at 2... setoid_rewrite K_red at 1... 
reflexivity.
Qed.

Hint Rewrite K_red using assumption : testDB.

(* auto works like intended if we do not need depth-first-rewriting *)
Lemma testAutoWorks s t: isVal s -> isVal t -> s (K s t) >> s s.
Proof.
  intros. autorewrite with testDB. reflexivity.
Qed.

(* but autorewrite fails here because it tries K_red at the first
occurrence of K,
but "K s t" is not an value, so constrains can not be solved.
And autorewrite does not try to use K_red at the second occurrence of
K, so this does not work.
*)
Lemma testAuto s t u: isVal s -> isVal t -> isVal u -> K (K s t) u >> s.
Proof.
  intros. autorewrite with testDB. (* no progress *)
Admitted.