The Coq mailing list

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

You can avoid the detour via Eqdep_dec (which is axiom free though)
using pattern matching but the type is difficult to write in 
"programming style" because of dependent pattern matching.

However, using "proof-style programming" (tactics), the type is
much easier to define/write. See the type definition RoofHom_inv_t
and the generated term.

Best,

Dominique

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

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.

Definition RoofHom_inv_t : forall x y, RoofHom x y -> Prop.
Proof.
  intros [] [] f.
  exact (f = IdNeg).
  exact False.          (* Unused, any Prop is ok here *)
  exact False.          (* Unused, any Prop is ok here *)
  exact (f = ZeroNeg).
  exact (f = IdZero).
  exact (f = ZeroPos).
  exact False.          (* Unused, any Prop is ok here *)
  exact False.          (* Unused, any Prop is ok here *)
  exact (f = IdPos).
Defined.

(* This is the term in programming style ... *)

Print RoofHom_inv_t.

Fact RoofHom_inv x y f : RoofHom_inv_t x y f.
Proof.
  destruct f; reflexivity.
Qed.

Lemma RNeg_RNeg_id (f : RoofHom RNeg RNeg) : f = IdNeg.
Proof. exact (RoofHom_inv _ _ f). Qed.

Lemma RZero_RPos_id (f : RoofHom RZero RPos) : f = ZeroPos.
Proof. exact (RoofHom_inv _ _ f). Qed.

----- Mail original -----
> De: "Dominique Larchey-Wendling" 
> <dominique.larchey-wendling AT loria.fr>
> À: 
> coq-club AT inria.fr
> Envoyé: Vendredi 26 Mai 2017 19:39:30
> Objet: Re: [Coq-Club] Avoiding the use of JMeq_eq
> 
> 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
> > 
>