The Coq mailing list

["JAEGER, Eric (SGDN)" <eric.jaeger AT sgdn.gouv.fr>]

Hi again,

Attached below is a piece of code that tries to capture the problem I have 
in a simplified manner.

I use a type lift_nat with a coercion from nat to lift_nat, and wants to 
perform a simplification of functional
expressions - not using "simpl" but "lift_simpl" (to keep coercions, 
notations, and so on, because the simplified
versions of such expressions in my development are much uglier than the 
original ones).

The first try is the tactic "my_simpl1", that just does not work. As 
mentionned by Matthieu, this is probably related
to the absence of typechecking and therefore the absence of coercions 
preventing the match.

The version "my_simpl2" is more generic, capturing ANY use of the function, 
but then trying to apply "lift_simpl".
Note that while the pattern matching does not cause reductions 
(conversions), trying to apply lift_simpl may have
such side-effects. Indeed, for example if I have "H:lift_alwaystrue n=true", 
I can do "generalize (lift_simpl _ H)";
the term "(lift_simpl _ H)" implies a reduction... That's the type of 
reduction I would like to avoid, because my
tactic is far less precise than I've expected (I do not blame Ltac, but my 
use of Ltac) - indeed, the match capture
any use of the function, but I would like then to try applying lift_simpl to 
discriminate hypotheses that can be
simplified, and only those.

The version "my_simpl3" is again derived from "my_simpl1", but making 
explicit the coercion, and
"my_simpl4" is derived from "my_simpl2".

my_simpl2, 3 and 4 succeed in proving theorem test. Unfortunately I've to 
use them several times, because using "repeat" causes a crash. Using the 
proposal of Yves (generalising, clearing) I may avoid the problem.

Yet I do not understand the behaviour of my_simpl2, 3 and 4 in test'... How 
may I have different messages, one
indicating success, the other failure? There is backtracking going on here, 
but that does not give me any clue about what is happening.

I hope to be clearer now ;-)

   Regards, Eric

==========================================

Inductive lift_nat:Set := ln:nat->lift_nat.
Coercion ln:nat>->lift_nat.
Fixpoint alwaystrue(n:nat){struct n}:bool :=
match n with
| O => true
| S n'=> alwaystrue n'
end.
Definition lift_alwaystrue(n:lift_nat):bool := match n with ln n' => 
alwaystrue n' end.

Theorem lift_simpl:forall (n:nat), lift_alwaystrue(S 
n)=true->lift_alwaystrue(n)=true.
Proof.
intros n HS; apply HS.
Qed.

Ltac my_simpl1:=
match goal with
| Hfr:(lift_alwaystrue (S _)=_) |- _ => generalize (lift_simpl _ Hfr); 
clear Hfr; intros Hfr;
                                        idtac "my_simpl1: match"
| _ => idtac "my_simpl1: no match"
end.

Ltac my_simpl2:=
match goal with
| Hfr:(lift_alwaystrue (_)=_) |- _ => (generalize (lift_simpl _ Hfr); clear 
Hfr; intros Hfr;
                                       idtac "my_simpl2: match ok") ||
                                       idtac "my_simpl2: match fail"
| _ => idtac "my_simpl2: no match"
end.

Ltac my_simpl3:=
match goal with
| Hfr:(lift_alwaystrue (ln (S _))=_) |- _ => (generalize (lift_simpl _ 
Hfr); clear Hfr; intros Hfr;
                                              idtac "my_simpl3: match ok") 
||
                                              idtac "my_simpl3: match fail"
| _ => idtac "my_simpl3: no match"
end.

Ltac my_simpl4:=
match goal with
| Hfr:(lift_alwaystrue (ln _)=_) |- _ => (generalize (lift_simpl _ Hfr); 
clear Hfr; intros Hfr;
                                          idtac "my_simpl4: match ok") ||
                                          idtac "my_simpl4: match fail"
| _ => idtac "my_simpl4: no match"
end.

Theorem test:forall (n:nat), lift_alwaystrue(S (S 
n))=true->lift_alwaystrue(n)=true.
Proof.
intros n H.
(* my_simpl1. -- Prompts "my_simpl1: no match", does nothing *)
(* my_simpl2. -- Prompts "my_simpl2: match ok", simplifies H *)
(* my_simpl3. -- Prompts "my_simpl3: match ok", simplifies H *)
(* my_simpl4. -- Prompts "my_simpl4: match ok", simplifies H *)
my_simpl2; my_simpl2; apply H.
Qed.

Variable g:nat->nat.

Theorem test':forall (n:nat), lift_alwaystrue(g 
n)=true->lift_alwaystrue(n)=true.
Proof.
intros n H.
(* my_simpl1. -- Prompts "my_simpl1: no match", does nothing *)
(* my_simpl2. -- Prompts "my_simpl2: match ok" AND "my_simpl2:match fail", 
does nothing *)
(* my_simpl3. -- Prompts "my_simpl3: no match", does nothing *)
(* my_simpl4. -- Prompts "my_simpl4: match ok" AND "my_simpl2:match fail", 
does nothing *)
Admitted.


----- Original Message ----- 
From: "Yves Bertot" <Yves.Bertot AT sophia.inria.fr>
To: "JAEGER, Eric (SGDN)" 
<eric.jaeger AT sgdn.gouv.fr>
Cc: "Matthieu Sozeau" 
<Matthieu.Sozeau AT lri.fr>;
 
<coq-club AT pauillac.inria.fr>
Sent: Tuesday, February 03, 2009 10:18 AM
Subject: Re: [Coq-Club] Question about tactics and conversions


> > Indeed, may be I should make explicit coercions in my tactic : f(COER t) 
> > instead of f(t). If the pattern matching does not typecheck it may not be 
> > fully aware of coercions (coercions being, if I understood correctly, 
> > introduced as required to typecheck)... and may try to reduce expressions 
> > to match, and that is probably the source of my difficulty.
> >
> >    Regards, Eric
> Well, as Mathieu said, there should not be any reduction happening.  This 
> should not be the problem...