Skip to content

Instantly share code, notes, and snippets.

@knuton

knuton/Trans.v

Created January 26, 2014 20:55
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save knuton/8639349 to your computer and use it in GitHub Desktop.
Save knuton/8639349 to your computer and use it in GitHub Desktop.
Download ZIP
Illustration of a problem with transitive relations in Coq
Raw
Trans.v
Require Import Omega.
Require Import Coq.Setoids.Setoid.
Inductive trans_r : nat -> nat -> Prop :=
| trans_r_base : trans_r 0 3
| trans_r_plus : forall m n, trans_r m n -> trans_r (m+3) (n+3)
| trans_r_trans : forall m n o, trans_r m n -> trans_r n o -> trans_r m o.
Example trans_r_6_9 : trans_r 3 9.
Proof.
assert (TRIV1: 3 = 0 + 3). compute. reflexivity.
assert (TRIV2: 6 = 3 + 3). compute. reflexivity.
assert (TRIV3: 9 = 6 + 3). compute. reflexivity.
apply trans_r_trans with (n := 6).
rewrite TRIV1 at 1. rewrite TRIV2. apply trans_r_plus. apply trans_r_base.
rewrite TRIV2 at 1. rewrite TRIV3. apply trans_r_plus.
rewrite TRIV1 at 1. rewrite TRIV2. apply trans_r_plus. apply trans_r_base.
Qed.
Example not_trans_r_1_2 : ~ trans_r 1 2.
Proof.
unfold not. intro. inversion H.
(* trans_r_base is automatically eliminated *)
(* trans_r_plus is no problem *)
contradict H0. omega.
(* trans_r_trans poses a problem *)
(* No matter which of the transitivity premisses we try to eliminate,
we seem to infinitely expand one of their premisses in trying to
disprove them. *)
inversion H0.
(* The first generated subgoal is again easy (it's just trans_r_plus). *)
contradict H4. omega.
(* But now we again need to deal with trans_r_trans just the same. *)
Abort.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment