coq.ipynb

graphtest.v

Inductive word :=
  | start : word
  | X : word -> word
  | Y : word -> word
  | Z : word -> word.


Inductive path : word -> Prop :=
  | s : path (X start)
  | a1 : forall w:word, path (X w) -> path (Y (X w))
  | a2 : forall w:word, path (X w) -> path (Z (X w))
  | b : forall w:word, path (Y w) -> path (Z (Y w))
  | c : forall w:word, path (Z w) -> path (X (Z w)).

Print path_ind.

Theorem xyz : path (Z (Y (X start))).
Proof.
repeat constructor. Qed.

Theorem xzx : path (X (Z (X start))).
Proof.
repeat constructor. Qed.

Print xzx.