1
$\begingroup$

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.

$\endgroup$
11
  • $\begingroup$ Have you tried proving a lemma saying that two parse trees over the same regular expession and list are equal? $\endgroup$ May 11, 2023 at 6:54
  • $\begingroup$ Your definition of prefer seems strange there is no base case. $\endgroup$
    – Lolo
    May 11, 2023 at 7:00
  • $\begingroup$ @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 $\endgroup$ May 11, 2023 at 14:49
  • $\begingroup$ @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. $\endgroup$ May 11, 2023 at 14:58
  • $\begingroup$ 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? $\endgroup$ May 11, 2023 at 19:33

1 Answer 1

2
$\begingroup$

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

$\endgroup$
2
  • $\begingroup$ This seems to be more involved than I thought it was :( $\endgroup$ May 18, 2023 at 11:08
  • $\begingroup$ 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 $\endgroup$ Jun 2, 2023 at 16:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.