The Coq mailing list

[roconnor AT theorem.ca]

On Thu, 7 Apr 2005, Pierre Casteran wrote:

> Hello,
>
>  Sometimes apply and constant unfolding don't cooperate as I expect.
> Let us take a simplified example.
>
> Inductive T2 : Set :=
>   zero : T2
> | cons : T2 -> T2 -> nat -> T2 -> T2.
>
> Definition psi (alpha beta:T2) := cons alpha beta 0 zero.
>
> Parameter lt : T2 -> T2 -> Prop.
>
> Axiom b_lt_psi_ab : forall a b , lt b (psi a b).
>
> (*
> Let us assume I want to solve the following goal :
> *)
>
> Goal forall a b , lt b (cons a b 0 zero).
>
>  intros; apply b_lt_psi_ab.
> (*
> Toplevel input, characters 581-598
> > intros; apply b_lt_psi_ab.
> >         ^^^^^^^^^^^^^^^^^
> Error: Impossible to unify "lt ?4 (psi ?3 ?4)" with "lt b (cons a b 0 zero)"
>
>  *)

Perhaps use the following:

Goal forall a b , lt b (cons a b 0 zero).
intros.
refine (b_lt_psi_ab _ _).
Qed.

or if you want something a yucky, but a bit more general:

Ltac use e :=
first
[refine (e)
|refine (e _)
|refine (e _ _)
|refine (e _ _ _)
|refine (e _ _ _ _)
|refine (e _ _ _ _ _)
|refine (e _ _ _ _ _ _)
|refine (e _ _ _ _ _ _ _)
|refine (e _ _ _ _ _ _ _ _)
|refine (e _ _ _ _ _ _ _ _ _)].

Goal forall a b , lt b (cons a b 0 zero).
intros.
use b_lt_psi_ab.
Qed.

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''