How to deduce this equality based on the fact that these two terms must be the same?

Question

Brief (but possibly inaccurate) Summary:

I have a proposition H : Prop1 p q. When I use inversion on the proposition, I get something like t1 : tree p and t2 : tree q. However, when I have Prop1 p p, I cannot get Coq to realize that t1 = t2.

Gist link to proof script

---

I have a definition of a SimpleRegex with characters and concatenation. They are defined as follows:

Inductive SimpleRegex : Type :=
| CharClass : (A -> bool) -> SimpleRegex
| Concat : SimpleRegex -> SimpleRegex -> SimpleRegex
.

Inductive parse_tree : SimpleRegex -> list A -> Type :=
| parse_charclass : forall f x,
    f x = true ->
    parse_tree (CharClass f) [x]
| parse_concat : forall r1 r2 s1 s2,
    parse_tree r1 s1 ->
    parse_tree r2 s2 ->
    parse_tree (Concat r1 r2) (s1 ++ s2)
.

I want to define a prefer relation that sets up a lexicographic order.

Inductive prefer : forall (r : SimpleRegex) (w1 w2 : list A),
    parse_tree r w1 -> parse_tree r w2 -> Prop :=
| prefer_concat_lex1 :
    forall (r s : SimpleRegex) (wr1 wr2 ws1 ws2 : list A)
    (pwr1 : parse_tree r wr1) (pwr2 : parse_tree r wr2)
    (pws1 : parse_tree s ws1) (pws2 : parse_tree s ws2),
    prefer r wr1 wr2 pwr1 pwr2 
    -> prefer (Concat r s) (wr1 ++ ws1) (wr2 ++ ws2) 
        (parse_concat r s wr1 ws1 pwr1 pws1) (parse_concat r s wr2 ws2 pwr2 pws2)
| prefer_concat_lex2 :
    forall (r s : SimpleRegex) (wr ws1 ws2 : list A)
    (pwr : parse_tree r wr)
    (pws1 : parse_tree s ws1) (pws2 : parse_tree s ws2),
    prefer s ws1 ws2 pws1 pws2
    -> prefer (Concat r s) (wr ++ ws1) (wr ++ ws2)
        (parse_concat r s wr ws1 pwr pws1) (parse_concat r s wr ws2 pwr pws2)
.

A plain english description of the two rules are (roughly) as follows:

1. Suppose r and s are SimpleRegexes, and wr1, wr2 ∈〖r〗 and ws1, ws2 ∈〖s〗. If we prefer a parse tree prw1 witnessing wr1 ∈〖r〗 more than prw2 witnessing wr2 ∈〖r〗, then parse_concat prw1 psw1 is preferred to parse_concat prw2 psw2 as parse trees.
2. Suppose r and s are SimpleRegexes, and ws1, ws2 ∈〖s〗. Then, for any wr ∈〖r〗, with parse tree pwr, the parse tree parse_concat pwr psw1 is preferred to parse_concat pwr psw2 as parse trees.

I want to prove the following Proposition

Lemma prefer_antirefl : forall r w (p : parse_tree r w),
    ~ prefer r w w p p.

It is easy to get started.

Lemma prefer_charclass_antirefl :
    forall (c : A -> bool) (w : list A) (p : parse_tree (CharClass c) w),
    ~ prefer (CharClass c) w w p p.
Proof.
    unfold not. intros.
    remember (CharClass c) as r.
    destruct p; inversion Heqr.
    - inversion H.
Qed.

Lemma prefer_antirefl : forall r w (p : parse_tree r w),
    ~ prefer r w w p p.
Proof.
    unfold not. induction r; intros.
    - now apply prefer_charclass_antirefl in H.
    - remember (Concat r1 r2) as r.
      destruct p; inversion Heqr.
      (* This inversion above does away with all the cases 
         where p is not related to Concat
      *)
      inversion H. subst.
      + admit.
      + admit.
Admitted.

At the point of the first admit, I have the following:

A: Type
r1, r2: SimpleRegex
IHr1: forall (w : list A) (p : parse_tree r1 w), prefer r1 w w p p -> False
IHr2: forall (w : list A) (p : parse_tree r2 w), prefer r2 w w p p -> False
Heqr: Concat r1 r2 = Concat r1 r2
s1, s2: list A
p1: parse_tree r1 s1
p2: parse_tree r2 s2
H: prefer (Concat r1 r2) (s1 ++ s2) (s1 ++ s2)
      (parse_concat r1 r2 s1 s2 p1 p2) (parse_concat r1 r2 s1 s2 p1 p2)
pwr3, pwr0: parse_tree r1 s1
H3: prefer r1 s1 s1 pwr0 pwr3
H5, H6, H7: s1 ++ s2 = s1 ++ s2
pws0: parse_tree r2 s2

Unfortunately, Coq does not realize that pwr3 and pwr0 must be the same tree since they came from the same parse_concat tree in H.

How do I inform Coq of this, and close the proof?

Gist Available Here (RegexParseTreesSimple.v)

---

Edit: I thought I should edit to clarify the question I am asking, and answer some of the questions in the comments.

Question 1:

I have the following hypothesis H

H: prefer (Concat r1 r2) (s1 ++ s2) (s1 ++ s2)
      (parse_concat r1 r2 s1 s2 p1 p2) (parse_concat r1 r2 s1 s2 p1 p2)

where s1, s2 are the strings, p1, p2 are the parse trees.

Notice that the last two arguments of H are syntactically the same. Since the rule prefer_concat_lex1 to construct H, applying inversion on H should give us p1, p2 back and a proposition prefer r1 s1 s1 p1 p1. Unfortunately, instead of finding p1 and p2 by pattern matching the parse_concats, Coq comes up with two new pwr3, pwr0, of which we know nothing.

How do I get Coq to give us the hypothesis prefer r1 s1 s1 p1 p1?

Question 2: If this is impossible, how do I prove prefer_antirefl as stated above?

Clarification: User Lolo says

Your definition of prefer seems strange there is no base case.

Indeed that is true. In my full version, I do have a base case, but I have tried to find a minimal complete example for the purpose of this example to replicate the issue.

Answer 1

This is a dependent inversion problem that has been bothering many Coq users. There is a short answer on Stack Overflow [1].

For your example, we have H before inversion:

H : prefer (Concat r0 r3) (app s1 s2) (app s1 s2) (parse_concat r0 r3 s1 s2 p1 p2)
      (parse_concat r0 r3 s1 s2 p1 p2)

After inversion H, we have pwr0, pwr3 : parse_tree r0 s1. We know they both come from p1, so they should be equal. But actually they are linked to p1 as

H10 : existT (fun r1 : SimpleRegex => {s1 : list A & parse_tree r1 s1}) r0
        (existT (fun s1 : list A => parse_tree r0 s1) s1 pwr0) =
      existT (fun r1 : SimpleRegex => {s1 : list A & parse_tree r1 s1}) r0
        (existT (fun s1 : list A => parse_tree r0 s1) s1 p1)
H15 : existT (fun r1 : SimpleRegex => {s1 : list A & parse_tree r1 s1}) r0
        (existT (fun s1 : list A => parse_tree r0 s1) s1 pwr3) =
      existT (fun r1 : SimpleRegex => {s1 : list A & parse_tree r1 s1}) r0
        (existT (fun s1 : list A => parse_tree r0 s1) s1 p1)

Coq's type system does not allow us to directly derive pwr0 = p1 and pwr3 = p1. I don't know why it is not allowed, but I find we can only derive from existT P x a = existT P x b to eq_rect x P a x H = b (an induced version of a equals b, instead of a itself), but not a = b, using inversion_sigma [2].

Require Import Coq.Logic.Eqdep_dec.

Context (A : Type) (P : A -> Type) (x : A).

Goal forall a b : P x,
  existT P x a = existT P x b -> a = b.
Proof.
  intros. inversion_sigma H.

If we can prove H = @eq_refl A x (axiom K [3]), then eq_rect x P a x H evaluates to a:

  assert (H = eq_refl) by admit.
  subst H.
  simpl in H0.
  apply H0.

If equality of SimpleRegex is decidable, which should be the case, you can use inj_pair2_eq_dec [1] to resolve your problem. Otherwise, you might want to accept axiom K.

[1] https://stackoverflow.com/questions/24720137/inversion-produces-unexpected-existt-in-coq

[2] https://coq.inria.fr/refman/proofs/writing-proofs/reasoning-inductives.html#coq:tacn.inversion_sigma

[3] https://coq.inria.fr/files/adt-2fev10-corbineau.pdf