The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Much like for the transparent assert I just replied to: this makes sense in trunk, but is currently unavailable due to technical difficulties. Sorry to keep you waiting.


Arnaud Spiwack

On 9 September 2011 14:22, Hendrik Tews <tews AT os.inf.tu-dresden.de> wrote:

Hi,

I am looking for a variants of rewrite and apply that generate
subgoals for dependent premises whose type is in Prop, if the
unification does not yield an instance.

Alternatively I am looking for a variant of erewrite and eapply
that turn existential variables of a type in Prop into subgoals.

For a small, artificial example, consider


Require Import Arith.

Parameter f : forall(n : nat)(pos : n > 0), nat.
(* f is simply a partial function, whose value
 * does not depend on the argument pos.
 *)

Axiom fvalue_tcc : forall(n : nat), n > 1 -> n - 1 > 0.

Axiom fvalue : forall(n : nat)(pos : n > 0)(gt1 : n > 1),
 f n pos = f (n - 1) (fvalue_tcc n gt1).
(* This is a rewrite rule for f. Here pos is universally
 * quantified, because the rule should apply to all witnesses
 * of n > 0.  n > 1 is a simple precondition for the rule.
 * It only gets a name here, because I have to construct
 * the witness for the f on the right-hand side.
 *)

Lemma lemma : f 2 (gt_Sn_O 1) = 0.
Proof.
(* Here I would like to rewrite with fvalue, but in such a way
 * that I get an additional subgoal 2 > 1, whose proof will
 * provide the instantiation for argument gt1.
 * erewrite does not really help here, because the created
 * existential will most likely disappear without getting
 * instantiated.
 *)

Thanks in advance,

Hendrik