Library examples.cime_trace.terminaison
Require Omega.
Require Import Relations.
Require Import Wellfounded.
Set Implicit Arguments.
Section star.
Unset Implicit Arguments.
Variable A:Set.
Variable R : A -> A -> Prop.
Inductive star (x:A) : A -> Prop :=
| star_refl : star x x
| star_step : forall y, star x y -> forall z, R y z -> star x z
.
Lemma star_trans: forall x y z, star x y -> star y z -> star x z.
Proof.
intros x y z H H1;revert x H;
induction H1.
tauto.
intros.
econstructor 2 with y0;auto.
Qed.
Lemma star_R : forall x y, R x y -> star x y.
Proof.
intros x y H;constructor 2 with x;[constructor|assumption].
Qed.
End star.
Ltac prove_star :=
match goal with
| |- star _ _ ?t ?t => exact rt_refl
| H:star _ _ ?t' ?t |- star _ _ ?t' ?t => assumption
| H:star _ _ ?t'' ?t |- star _ _ ?t' ?t =>
(apply star_trans with t'';[prove_star|exact H]) ||
(clear H;prove_star)
| H:star _ _ ?t' ?t'' |- star _ _ ?t' ?t =>
(apply star_trans with t'';[exact H|prove_star]) ||
(clear H;prove_star)
| H:?R ?t' ?t |- star _ _ ?t' ?t => apply star_R;exact H
| H:?R ?t'' ?t |- star _ _ ?t' ?t =>
(apply star_trans with t'';[prove_star|apply star_R;exact H]) ||
(clear H;prove_star)
| H:?R ?t' ?t'' |- star _ _ ?t' ?t =>
(apply star_trans with t'';[apply star_R;exact H|prove_star]) ||
(clear H;prove_star)
| _ => complete eauto
end.