Commit 5e6e9a20 authored by Robbert's avatar Robbert

Merge branch 'robbert/involutive' into 'master'

Define `Involutive` in terms of `Cancel`.

See merge request iris/stdpp!79
parents a426377a 9fbe44b6
Pipeline #17985 passed with stage
in 10 minutes and 5 seconds
......@@ -327,8 +327,11 @@ Class Trichotomy {A} (R : relation A) :=
trichotomy x y : R x y x = y R y x.
Class TrichotomyT {A} (R : relation A) :=
trichotomyT x y : {R x y} + {x = y} + {R y x}.
Class Involutive {A} (R : relation A) (f : A A) :=
involutive x : R (f (f x)) x.
Notation Involutive R f := (Cancel R f f).
Lemma involutive {A} {R : relation A} (f : A A) `{Involutive R f} x :
R (f (f x)) x.
Proof. auto. Qed.
Arguments irreflexivity {_} _ {_} _ _ : assert.
Arguments inj {_ _ _ _} _ {_} _ _ _ : assert.
......@@ -346,7 +349,6 @@ Arguments anti_symm {_ _} _ {_} _ _ _ _ : assert.
Arguments total {_} _ {_} _ _ : assert.
Arguments trichotomy {_} _ {_} _ _ : assert.
Arguments trichotomyT {_} _ {_} _ _ : assert.
Arguments involutive {_ _} _ {_} _ : assert.
Lemma not_symmetry `{R : relation A, !Symmetric R} x y : ¬R x y ¬R y x.
Proof. intuition. Qed.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment