The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

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)"

 *)
Abort.

(*
A solution which seems to work and can be quite generic is the following one:
*)

Ltac apply_unfold cst thm :=
    generalize thm ; let H  := fresh in
                                 (intro H; unfold cst in H; apply H).


Goal forall a b , lt b (cons a b 0 zero).
 intros; apply_unfold psi b_lt_psi_ab.
Qed.


Unfortunately it is not easy to generalize this tactic for unfolding
at some given positions. One can use something like "fold (psi a b)"
but if a and b are replaced with big terms, that can be quite heavy to use.
I didn't find in the manual options like "unfold ... in ..."
nor options for unfoldings constants before applying a term.


Is there a simpler solution ?

Pierre


-- 
Pierre Casteran

http://www.labri.fr/Perso/~casteran/

(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.