The Coq mailing list

[Jeffrey Terrell <jeff AT abstractsolutions.co.uk>]

Hi,

I'd be grateful for some help in proving T. I'm aware that the outer "match" is 
redundant but would like to retain it for the time being. Thanks.

Regards,
Jeff.

(* A source class. *)

Inductive C : Type :=
   Build_C : forall _ : Set, option C -> C.

(* A target class, with pre and post conditions. *)

Inductive D : Type :=
   Build_D : forall S : Set, forall T : Set,
      (S -> Prop) -> (S -> T -> Prop) -> option D -> D.

(* The relation "source class is transformed into target class". *)

Inductive Pot : C -> D -> Type :=

Leaf :
   forall S : Set,
   forall T : Set,
   forall Pre : (S -> Prop),
   forall Post : (S -> T -> Prop),
      Pot (Build_C S None) (Build_D S T Pre Post None) |

Branch :
   forall c : C,
   forall d : D,
      Pot c d ->
         forall S : Set,
         forall T : Set,
         forall Pre : (S -> Prop),
         forall Post : (S -> T -> Prop),
            Pot (Build_C S (Some c)) (Build_D S T Pre Post (Some d)).

(* The specification of a transformation between a source and a
target class. *)

Fixpoint Tran (c : C) (d : D) (p : Pot c d) {struct p} : Prop :=
   match p with |

      Leaf S' T Pre Post =>
         forall s : S', Pre s -> exists t : T, Post s t |

      Branch c' d' p' S' T Pre Post =>
         forall s : S', Pre s -> exists t : T, Post s t /\ Tran c' d' p'
   end.

(* All transformations are provable. *)

Theorem T :
   forall c : C,
   forall d : D,
   forall p : Pot c d,
      match c with Build_C _ _ =>
         match d with Build_D S' T Pre Post _ =>
            forall Proof : (forall s : S', Pre s -> exists t : T, Post s t),
               Tran c d p
         end
      end.

Proof.
intros.
induction p.
simpl.
trivial.
simpl.
intros.
destruct (Proof s H).
exists x.
split.
assumption.