Skip to content

Instantly share code, notes, and snippets.

@Lysxia

Lysxia/Rw.v

Created November 7, 2019 00:19
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 Lysxia/900b38b7d141ccfd56ffe988e27f6605 to your computer and use it in GitHub Desktop.
Save Lysxia/900b38b7d141ccfd56ffe988e27f6605 to your computer and use it in GitHub Desktop.
Download ZIP
Trivial example of rewrite with non-transitive relation
Raw
Rw.v
From Coq Require Import Setoid Morphisms.
Inductive Trivial (n : nat) : Prop := T.
Definition neq : nat -> nat -> Prop :=
fun n m => n <> m.
Lemma neq_0_1 : neq 0 1.
Proof.
discriminate.
Qed.
Instance Proper_Trivial
: Proper (neq ==> iff) Trivial.
Proof.
firstorder.
Qed.
Theorem Trivial_1 : Trivial 1.
Proof.
rewrite <- neq_0_1.
constructor.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment