Install

General tips

Examples

(* simple language with minus operator *)
Inductive ex : Set := 
   | ex_zero : ex 
   | ex_one : ex
   | ex_minus : ex -> ex -> ex.

Inductive eval : ex -> nat -> Prop :=
   | eval_zero : eval ex_zero 0
   | eval_one : eval ex_one 1
   | eval_minus : forall e1 e2 n1 n2,
     eval e1 n1 ->
     eval e2 n2 ->
     eval (ex_minus e1 e2) (n1 - n2).

Notation "e => n" := (eval e n) (at level 68).

Lemma uniquness : forall e n1 n2,
   e => n1 /\ e => n2 -> n1 = n2.
Proof.
  induction e.
  (* ex_zero *) intros. inversion H. inversion H0. inversion H1. auto. 
  (* ex_one *) intros. inversion H. inversion H0. inversion H1. auto.
  (* ex_minus *) intros. inversion H. inversion H0. inversion H1. auto.
Qed.

(* transition relation *)
Variable A : Type.
Variable R : A -> A -> Prop.

Definition Rstar (x y:A) :=
    forall P:A -> A -> Prop,
      (forall u:A, P u u) -> (forall u v w:A, R u v -> P v w -> P u w) -> P x y.

 Theorem Rstar_reflexive : forall x:A, Rstar x x.
 Proof.
    unfold Rstar. intros x P P_refl RoP. apply P_refl.
 Qed.

 Theorem Rstar_R : forall x y z:A, R x y -> Rstar y z -> Rstar x z.
 Proof.
    intros x y z R_xy Rstar_yz.
    unfold Rstar.
    intros P P_refl RoP. apply RoP with (v:=y).
      assumption.
      apply Rstar_yz. assumption. assumption.
 Qed.

Theorem Rstar_transitive :
    forall x y z:A, Rstar x y -> Rstar y z -> Rstar x z.
Proof.
    intros x y z Rstar_xy; unfold Rstar in Rstar_xy.
    apply Rstar_xy; trivial.
    intros u v w R_uv fz Rstar_wz.
    apply Rstar_R with (y:=v); auto.
Qed.