1
$\begingroup$

Is there a simple way to use rewrites inside quantified Props? As an example, consider the following:

Goal forall (xs : list nat) (ys : list nat),
  (forall x, In x (xs ++ ys) -> x < 10) -> True.
Proof.
  intros.

makes the context look like

A: Type
xs, ys: list nat
H: forall x : nat, In x (xs ++ ys) -> x < 10

Now, recall that

in_app_iff
     : forall (A : Type) (l l' : list A) (a : A),
       In a (l ++ l') <-> In a l \/ In a l'

However, rewrite in_app_iff in H. gives me an error:

Found no subterm matching "In ?y (?l ++ ?l0)" in the current goal.

I want it to transform the context into

H: forall x : nat, (In x xs \/ In x ys) -> x < 10

I am aware that I can do this by first specializing x inside an assert environment or something, but it would be really nifty if I didn't have to do that.

$\endgroup$

1 Answer 1

2
$\begingroup$

Yes, the tactic setoid_rewrite lets you rewrite under binders. Here is the reference manual link.

For your example this gives:

From Coq Require Import List.
Goal forall (xs : list nat) (ys : list nat),
  (forall x, In x (xs ++ ys) -> x < 10) -> True.
Proof.
  intros xs ys H.

The context is

xs, ys : list nat
H : forall x : nat, In x (xs ++ ys) -> x < 10
========================= (1 / 1)
True

then writing

  setoid_rewrite in_app_iff in H.

gives you

xs, ys : list nat
H : forall x : nat, In x xs \/ In x ys -> x < 10
========================= (1 / 1)
True
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.