The Coq mailing list

[jandronick <jandronick AT axalto.com>]

Hi Pierre,
In fact my goal is more complicated, with more hypothsese and more "and". Let 
us look the following one:
-----------
Parameter P : nat -> Prop.
Parameter Q : nat -> Prop.
Parameter R : nat -> Prop.
Parameter P_succ : forall n, P n -> P (S n).
Parameter Q_succ_succ : forall n, Q n -> Q (S (S n)).
Parameter is_ok : nat -> Prop.
Parameter R_def : forall n, (is_ok n) -> R n.

Goal forall n,
   (is_ok n) /\ ((P n)\/(Q n)) ->
  ((R n)  /\  (P(S n)\/Q(S(S n)))).
Proof.
  intuition; 
  apply R_def; auto. 
  left; apply P_succ; auto.
  apply R_def; auto. 
  right; apply Q_succ_succ; auto.
Qed.
---------
I must prove (R n) twice !
I agree that is this case, "intuition; try apply R_def; auto." would work, 
but 
what about if I have 
     ((R1 n)  /\  (R2 n)  /\ ... /\  (Rm n)  /\  (P(S n)\/Q(S(S n)))).
I have to put the proofs of all the goals, except (P(S n)\/Q(S(S n))) , in a 
"try" after the "intuition"...
Or I must decompose the hypotheses and the goal by hand, which is exactly 
what 
I am trying to avoid ! Here we could have:
-----
  intros. split.
    decompose [and] H; apply R_def; auto.
    intuition.
      left; apply P_succ; auto.
      right; apply Q_succ_succ; auto.
--------
But if I have the hypotheses, and the goal, with a lot of "and" and "or" and 
"exists" etc... it becomes heavy !!! 
I hope it's clearer...
Thanks !
June




Le vendredi 08 Avril 2005 10:46, Pierre Casteran a écrit :
> Bonjour June,
>
>  Did you mean something like that :
>
>
> Goal (0=1\/0=2)->(1=3/\2=2/\3=3/\4=4/\5=5).
>  intro.
> split;[idtac|clear H;intuition].
>  case H;discriminate 1.
> Save pf.
>
> Print pf.
> pf =
> fun H : 0 = 1 \/ 0 = 2 =>
> conj
>   match H return (1 = 3) with
>
>   | or_introl H0 =>
>
>       let H1 :=
>         eq_ind 0
>           (fun ee : nat => match ee with
>
>                            | O => True
>                            | S _ => False
>
>                            end) I 1 H0 in
>       False_ind (1 = 3) H1
>
>   | or_intror H0 =>
>
>       let H1 :=
>         eq_ind 0
>           (fun ee : nat => match ee with
>
>                            | O => True
>                            | S _ => False
>
>                            end) I 2 H0 in
>       False_ind (1 = 3) H1
>   end
>   (conj (refl_equal 2)
>      (conj (refl_equal 3) (conj (refl_equal 4) (refl_equal 5))))
>
>      : 0 = 1 \/ 0 = 2 -> 1 = 3 /\ 2 = 2 /\ 3 = 3 /\ 4 = 4 /\ 5 = 5
>
> Pierre
>
> Selon jandronick 
>Â <jandronick AT axalto.com>:
> > Hello,
> > Is their a way to exclude an hypothesis of the tactic intuition ?
> > I mean, if I have :
> >     H : A \/ B
> >    -------------
> >    P1 /\ P2 /\ P3 /\ P4 /\ P5
> > and that I need to distinguish the case A of the case B only to prove P1,
> > I would like to do something like "intuition except H" not to be obliged
> > to prove P2, ..., P5 in the case A and prove again P2, ..., P5 for the
> > case B... I hope it is clear for someone... ;-)
> > June
> >
> > --------------------------------------------------------
> > Bug reports: http://coq.inria.fr/bin/coq-bugs
> > Archives: http://pauillac.inria.fr/pipermail/coq-club
> >           http://pauillac.inria.fr/bin/wilma/coq-club
> > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

-- 
June Andronick
Formal Methods & Security
Advanced Research - Axalto
36-38 rue de la Princesse, B.P. 45
78431 Louveciennes Cedex, France
phone : +33 (0) 1 30 08 48 78
fax :   +33 (0) 1 30 08 45 24