The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Here is a solution using setoid rewriting (it may be a bit advanced though, and if you don't feel comfortable with setoid rewriting, follow Cedric's proof step)

Require Import Coq.Setoids.Setoid.

Ltac fold_impl h :=
  lazymatch type of h with
  | ?A->?B => change (Basics.impl A B) in h
  | _ => idtac
  end
.

Goal forall (P Q R:Prop), (P->Q) -> Q\/R.
Proof.
  intros P Q R H.
  fold_impl H.
  rewrite <- H.

On 20 August 2014 14:58, Cedric Auger <sedrikov AT gmail.com> wrote:

Yes, use of "assert" or "cut" tactic can be useful. I will not provide the proof script, as it is quite easy. If you still find it hard, you should really read some documentation (Software Foundations, or Certified Programming with Dependant Types, for instance). The Coq reference manual is also a valuable reference.

2014-08-20 14:53 GMT+02:00 .... <nixiejun AT 163.com>:

Dear Coq users:

    Here I meet a question.

    1 subgoals
P : Prop
Q : Prop
R : Prop
H : P -> Q
______________________________________(1/1)
Q \/ R

    

    Is it possible to use H:P->Q to transform subgoal Q\/R to P\/R. 

--
.../Sedrikov\...