The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi John,

I would do it using an general inversion lemma ... easy to prove
but more difficult to state ... and then use discriminate
and uniqueness of identity proofs for your decidable type.

Dominique

---------------------------------------

Require Import Eqdep_dec.

Inductive RoofObj : Type := RNeg | RZero | RPos.

Fact RoofObj_dec (x y : RoofObj) : { x = y } + { x <> y }.
Proof. decide equality. Qed.

Fact UIP_RoofObj (x : RoofObj) (H : x = x) : H = eq_refl.
Proof. apply UIP_dec, RoofObj_dec. Qed.

Inductive RoofHom : RoofObj -> RoofObj -> Type :=
    | IdNeg   : RoofHom RNeg  RNeg
    | ZeroNeg : RoofHom RZero RNeg
    | IdZero  : RoofHom RZero RZero
    | ZeroPos : RoofHom RZero RPos
    | IdPos   : RoofHom RPos  RPos.

Fact RoofHom_inv x y (f : RoofHom x y) : 
      (exists (Hx : x = RNeg)  (Hy : y = RNeg),  IdNeg   = eq_rect _ (RoofHom 
_) (eq_rect _ (fun x => RoofHom x y) f _ Hx) _ Hy)
   \/ (exists (Hx : x = RZero) (Hy : y = RNeg),  ZeroNeg = eq_rect _ (RoofHom 
_) (eq_rect _ (fun x => RoofHom x y) f _ Hx) _ Hy)
   \/ (exists (Hx : x = RZero) (Hy : y = RZero), IdZero  = eq_rect _ (RoofHom 
_) (eq_rect _ (fun x => RoofHom x y) f _ Hx) _ Hy)
   \/ (exists (Hx : x = RZero) (Hy : y = RPos),  ZeroPos = eq_rect _ (RoofHom 
_) (eq_rect _ (fun x => RoofHom x y) f _ Hx) _ Hy)
   \/ (exists (Hx : x = RPos)  (Hy : y = RPos),  IdPos   = eq_rect _ (RoofHom 
_) (eq_rect _ (fun x => RoofHom x y) f _ Hx) _ Hy).
Proof.
  destruct f; [ do 0 right | do 1 right | do 2 right | do 3 right | do 4 
right ]; try left;
    exists eq_refl, eq_refl; reflexivity.
Qed.

Lemma RNeg_RNeg_id (f : RoofHom RNeg RNeg) : f = IdNeg.
Proof.
  destruct (RoofHom_inv _ _ f) as 
      [   (Hx & Hy & E) 
      | [ (Hx & Hy & E) 
      | [ (Hx & Hy & E)
      | [ (Hx & Hy & E)
      |   (Hx & Hy & E) ] ] ] ]; try discriminate.
  rewrite (UIP_RoofObj _ Hx), (UIP_RoofObj _ Hy) in E.
  simpl in E; auto.
Qed.



----- Mail original -----
> De: "John Wiegley" 
> <johnw AT newartisans.com>
> À: 
> coq-club AT inria.fr
> Envoyé: Vendredi 26 Mai 2017 17:42:33
> Objet: [Coq-Club] Avoiding the use of JMeq_eq
> 
> I have a simple scenario where I'm representing "objects and arrows" as an
> inductive type, and another type that references the first one:
> 
>   Inductive RoofObj : Type := RNeg | RZero | RPos.
>   
>   Inductive RoofHom : RoofObj -> RoofObj -> Type :=
>     | IdNeg   : RoofHom RNeg  RNeg
>     | ZeroNeg : RoofHom RZero RNeg
>     | IdZero  : RoofHom RZero RZero
>     | ZeroPos : RoofHom RZero RPos
>     | IdPos   : RoofHom RPos  RPos.
> 
> This gives the structure of a "roof", or Λ, which is used to build span
> diagrams.
> 
> A trivial fact I need to prove that this is a category is the following 
> lemma
> (and others similar in form):
> 
>     Lemma RNeg_RNeg_id (f : RoofHom RNeg RNeg) : f = IdNeg.
> 
> However, destruct on 'f' gives me errors about abstracting over variables.
> "dependent destruction f" works, and completes the proof easily, but incurs
> the use of JMeq_eq.
> 
> I'm trying hard to keep this development free of axioms, so I found that the
> following specialized elimination principle will allow me to avoid JMeq_eq:
> 
>   Definition caseRoofNegNeg (p : RoofHom RNeg RNeg) :
>     forall (P : RoofHom RNeg RNeg -> Type)
>            (PIdNeg : P IdNeg), P p :=
>     match p with
>     | IdNeg => fun _ P => P
>     end.
>   
>   Lemma RNeg_RNeg_id (f : RoofHom RNeg RNeg) : f = IdNeg.
>   Proof.
>     pattern f.
>     apply caseRoofNegNeg.
>     reflexivity.
>   Qed.
> 
>   Print Assumptions RNeg_RNeg_id.
>   (* Look ma, no axioms. *)
> 
> Is this the best way of solving the problem? For larger categories there is 
> a
> lot of boilerplate in providing all these reduction rules, but it's worth it
> to avoid axioms. Though I thought perhaps, someone knows of a better way?
> 
> Thank you,
> --
> John Wiegley                  GPG fingerprint = 4710 CF98 AF9B 327B B80F
> http://newartisans.com                          60E1 46C4 BD1A 7AC1 4BA2
>