The Coq mailing list

[Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>]

[fun _ _ => bool] is an equivalence so it still doesn't work.

(Setoid is about relations in Prop, not crelations, so if you have proof 
irrelevance from some axiom the theorem is trivial.

If you don't have proof irrelevance the theorem implies it, see attached 
file)

Either you need to avoid relying on symmetry being involutive, or you 
need to take an hypothesis about it.

In the later case since you're using equivalences it might be worth 
looking at groupoids 
https://en.wikipedia.org/wiki/Groupoid#Category_theoretic where you have

f⁻¹⁻¹ = f⁻¹⁻¹ ∘ id
      = f⁻¹⁻¹ ∘ (f⁻¹ ∘ f)
      = (f⁻¹⁻¹ ∘ f⁻¹) ∘ f
      = id ∘ f
      = f

(if you need a coherence law on symmetry you may need ones for 
reflexivity and transitivity as well)

Gaëtan Gilbert

On 29/04/2017 10:16, John Wiegley wrote:
> > > > > > "GG" == Gaetan Gilbert 
> > > > > > <gaetan.gilbert AT ens-lyon.fr>
> > > > > >  writes:
> GG> [symmetry] is not involutive: take [R := fun _ _ => bool] and for the
> GG> proof of symmetry [fun x y (H : R x y) => true : R y x].
>
> GG> Then for some x and y, [false : R x y] and [symmetry (symmetry false) =
> GG> true <> false].
>
> Hi Gaëtan,
>
> How about relations that are known to be equivalences?
>
>    Theorem symmetry_invol `{Setoid A} (x y : A) (R : x === y) :
>      symmetry (symmetry R) = R.

Require Import RelationClasses.

Axiom symmetry_invol : forall A r (Heq : Equivalence r) (x y : A) (R : r x y),
    symmetry (symmetry R) = R.

Inductive boolP : Prop := trueP | falseP.

Lemma trueP_eq_falseP : trueP = falseP.
Proof.
pose (r := fun _ _ : unit => boolP).
unshelve refine (let Heq := _ : Equivalence r in _).
- split;red;[intros ?;exact trueP|idtac|intros ?????;exact trueP].
  intros x y _;exact trueP.
- exact (symmetry_invol _ r Heq tt tt falseP).
Qed.

Lemma proof_irrelevance (P : Prop) (p q : P) : p = q.
Proof.
pose (f := fun b => match b with trueP => p | falseP => q end).
change (f trueP = f falseP).
clearbody f.
rewrite trueP_eq_falseP. reflexivity.
Qed.