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

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.

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.


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.

• Have you tried proving a lemma saying that two parse trees over the same regular expession and list are equal? Commented May 11, 2023 at 6:54
• Your definition of prefer seems strange there is no base case.
– Lolo
Commented May 11, 2023 at 7:00
• @Lolo I presented a simpler version of my setup so that it is just large enough to represent the main problem I am stuck with Commented May 11, 2023 at 14:49
• @AndrejBauer I do not want to rely on such a lemma. I think what I want in this case should be possible anyway, because the last two arguments of prefer in H are syntactically the same thing. Commented May 11, 2023 at 14:58
• It's not possible. You should try proving the lemma, you'll discover that there is more to it than you think. For instance, if you have parse_charclass f x p and pase_charclass f x q where p : f x = true and q : f x = true, why do you think it follows p = q? Commented May 11, 2023 at 19:33

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.

• This seems to be more involved than I thought it was :( Commented May 18, 2023 at 11:08
• Is there some reason decidability is needed? I like my regexes to have predicates of the form (A -> bool) in the form of atomic characters, making equality undecidable Commented Jun 2, 2023 at 16:15