Proof (not-quite) irrelevance when when destructing coq equality

Question

I have a dependent type which models a finite path in a transition system. The transition system has a function R that yields a proposition saying whether there's an edge between states s and s' with label a. The finite path type is:

  Inductive FinPathTail (s : S i) :=
  | FPTNil: FinPathTail s
  | FPTCons (a : Act i) (s' : S i) : R i s a s' ->
                                     FinPathTail s' -> FinPathTail s.

(The "tail" bit is because this actually models all but the head of a path starting at s).

I've defined a CoInductive type for a possibly infinite PathTail (I'll stick it at the bottom so as to get to the question faster) and I have a function, fpt_to_pt, to transform a FinPathTail into a PathTail. This should "obviously" be injective, so I wanted to prove a lemma of this form:

Lemma fpt_to_pt_inj {s : S i} (fpt fpt' : FinPathTail s)
  : (forall s s' : S i, {s = s'} + {s <> s'}) ->
    fpt_to_pt fpt = fpt_to_pt fpt' -> fpt = fpt'.

When trying to prove this by induction on fpt, I quickly get to the case where both sides are known to be conses. The goal ends up looking something like:

PTCons s a s' r (fpt_to_pt fpt) = PTCons s a2 s'2 r2 (fpt_to_pt fpt') ->
FPTCons s a s' r fpt = FPTCons s a2 s'2 r2 fpt'

that I'd like to decompose with the injection tactic. The result ends up like this:

existT (fun s'0 : S i => PathTail s'0) s' (fpt_to_pt fpt) =
existT (fun s'0 : S i => PathTail s'0) s'2 (fpt_to_pt fpt') ->
s' = s'2 -> a = a2 -> FPTCons s a s' r fpt = FPTCons s a2 s'2 r2 fpt'

and using the inversion_sigma tactic, I can transform it to:

B : s' = s'2
C : a = a2
A0 : s' = s'2
A1 : eq_rect s' (fun a : S i => PathTail a) (fpt_to_pt fpt) s'2 A0 = fpt_to_pt fpt'

I think I understand why I need decidability for the source domain, in order to use inj_pair2_eq_dec. What I don't understand is: what happened to r and r2? I understand that I don't have proof irrelevance, but doesn't that mean that they must have been equal in order for the conses to be equal? Or am I misunderstanding something fundamental about propositions?

PS: Here's the coinductive definition for PathTail:

CoInductive PathTail (s : S i) :=
| PTNil: PathTail s
| PTCons (a : Act i) (s' : S i) : R i s a s' -> PathTail s' -> PathTail s.

Arthur Azevedo De Amorim Arthur Azevedo De Amorim · Accepted Answer · 2019-02-06T00:18:49

Apparently the injection tactic ignores equalities between proofs by default, but you can override this behavior with the Keep Proof Equalities flag:

Inductive foo : nat -> Prop :=
| Foo (n : nat) : foo n.

Inductive bar :=
| Bar (n : nat) : foo n -> bar.

Lemma test n nn m mm : Bar n nn = Bar m mm -> False.
Proof.
intros H. injection H. (* No equality generated. *)
Abort.

Set Keep Proof Equalities.

Lemma test n nn m mm : Bar n nn = Bar m mm -> False.
Proof.
intros H. injection H. (* Equality generated. *)
Abort.

Proof (not-quite) irrelevance when when destructing coq equality

1 Answers