The Coq mailing list

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

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
>


-- 
Pierre Casteran

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

(+33) 540006931

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