Search code examples
coqinduction

Induction order for relation between three lists

I'm working on a theory of string grammars, but I'm completely blocked by a particular theorem. Every induction ordering I've tried ends up stuck with nonsensical and useless induction hypotheses, and I'm not sure what I'm missing.

I've now reread this "Varying the Induction Hypothesis" section several times trying to understand what I'm doing wrong, but it seems I'm following their advice about generality just fine.

Simply put, I'm very confused. Your guidance is very much appreciated in advance!

Here's an overview of my definitions and the difficult theorem. I'll give my full script later.

(* I plan to make these definitions more complex in the future *)
Definition TokenDefinition := String.string.
Definition Token := String.string.
Definition TokenMatches (def: TokenDefinition) (token: Token): Prop := def = token.

Definition TokenPath := list TokenDefinition.
Definition TokenStream := list Token.

Inductive PathMatchesStream: TokenPath -> TokenStream -> Prop :=
    | PathMatchesStream_base: forall def token,
        TokenMatches def token
        -> PathMatchesStream [def] [token]
    | PathMatchesStream_append: forall def token path stream,
        TokenMatches def token
        -> PathMatchesStream path stream
        -> PathMatchesStream (def :: path) (token :: stream)
.

(* the problematic theorem *)
Theorem PathMatchesStream_same_if_match_same:
    forall a b stream,
        PathMatchesStream a stream
        -> PathMatchesStream b stream
        -> a = b.
Proof.
    (* my full script has many failed attempts *)
Qed.

Here's my full script, which should be runnable if you have Cpdt from Certified Programming with Dependent Types (I'm a huge convert to his style of automation).

Set Implicit Arguments. Set Asymmetric Patterns.
Require Import List.
Import ListNotations.
Open Scope list_scope.
Require String.
Require Import Cpdt.CpdtTactics.
Require Import PeanoNat Lt.

Definition TokenDefinition := String.string.
Definition Token := String.string.

Definition TokenMatches (def: TokenDefinition) (token: Token): Prop := def = token.
Hint Unfold TokenMatches: core.

Ltac simpl_TokenMatches :=
    unfold TokenMatches in *; subst.

Theorem TokenDefinition_match_same_then_same:
    forall a b token, TokenMatches a token -> TokenMatches b token -> a = b.
Proof. crush. Qed.


Definition TokenPath := list TokenDefinition.
Definition TokenStream := list Token.

Inductive PathMatchesStream: TokenPath -> TokenStream -> Prop :=
    | PathMatchesStream_base: forall def token,
        TokenMatches def token
        -> PathMatchesStream [def] [token]
    | PathMatchesStream_append: forall def token path stream,
        TokenMatches def token
        -> PathMatchesStream path stream
        -> PathMatchesStream (def :: path) (token :: stream)
.
Hint Constructors PathMatchesStream: core.

Ltac invert_PathMatchesStream :=
    crush; repeat match goal with
        | [ H : TokenMatches _ _ |- _ ] =>
            simpl_TokenMatches; crush
        | [ H : PathMatchesStream _ _ |- _ ] =>
            solve [inversion H; clear H; crush]
    end.

Theorem PathMatchesStream_path_not_empty:
    forall stream, ~(PathMatchesStream [] stream).
Proof. invert_PathMatchesStream. Qed.
Hint Resolve PathMatchesStream_path_not_empty: core.

Theorem PathMatchesStream_stream_not_empty:
    forall path, ~(PathMatchesStream path []).
Proof. invert_PathMatchesStream. Qed.
Hint Resolve PathMatchesStream_stream_not_empty: core.

Theorem PathMatchesStream_length_non_zero:
    forall path stream, PathMatchesStream path stream -> 0 < (length path) /\ 0 < (length stream).
Proof. invert_PathMatchesStream. Qed.
Hint Resolve PathMatchesStream_length_non_zero: core.

Theorem PathMatchesStream_same_if_match_same:
    forall a b stream,
        PathMatchesStream a stream
        -> PathMatchesStream b stream
        -> a = b.
Proof.

intros a; induction a as [| atok a IHa]; intros b; induction b as [| btok b IHb].

- invert_PathMatchesStream.
- invert_PathMatchesStream.
- invert_PathMatchesStream.

-
induction stream as [| tok stream IHstream].

+ invert_PathMatchesStream.


+
intros Ha Hb.

apply IHa.

(*intros a b stream Ha.
generalize dependent b.
induction Ha.
-
intros b Hb.
unfold TokenMatches in *.
induction Hb.
+

-




intros a.

induction a as [| atok a IHa].

- invert_PathMatchesStream.

-
intros b.
induction b as [| btok b IHb].
-- invert_PathMatchesStream.
--
intros stream.
induction stream as [| tok stream IHstream].
+ invert_PathMatchesStream.
+
intros Ha.
induction Ha; intros Hb; induction Hb.
++ apply IHb.
++ invert_PathMatchesStream.
++
inversion Ha; clear Ha; inversion Hb; clear Hb; invert_PathMatchesStream.
++
apply IHa.
++
*)

(*intros a b stream.
generalize dependent b.
generalize dependent a.
induction stream as [| tok stream IHstream].
- invert_PathMatchesStream.
-
intros a.
induction a as [| atok a IHa].
-- invert_PathMatchesStream.
--
intros b.
induction b as [| btok b IHb].
++ invert_PathMatchesStream.
++
intros Ha Hb.

induction Ha; induction Hb; simpl_TokenMatches.
crush.
invert_PathMatchesStream.*)

Qed.
Solution

  • For this theorem, you actually don't need anything too fancy. Just an auxiliary lemma:

    Require Import Coq.Lists.List.
Require Import Coq.Strings.String.
Import ListNotations.


(* I plan to make these definitions more complex in the future *)
Definition TokenDefinition := String.string.
Definition Token := String.string.
Definition TokenMatches (def: TokenDefinition) (token: Token): Prop := def = token.

Definition TokenPath := list TokenDefinition.
Definition TokenStream := list Token.

Inductive PathMatchesStream: TokenPath -> TokenStream -> Prop :=
    | PathMatchesStream_base: forall def token,
        TokenMatches def token
        -> PathMatchesStream [def] [token]
    | PathMatchesStream_append: forall def token path stream,
        TokenMatches def token
        -> PathMatchesStream path stream
        -> PathMatchesStream (def :: path) (token :: stream)
.

Theorem PathMatchesStream_same_if_match_same_aux :
    forall a stream, PathMatchesStream a stream -> a = stream.
Proof.
intros a b H.
now induction H; unfold TokenMatches in *; subst.
Qed.

(* the problematic theorem *)
Theorem PathMatchesStream_same_if_match_same:
    forall a b stream,
        PathMatchesStream a stream
        -> PathMatchesStream b stream
        -> a = b.
Proof.
now intros
   ? ? ? ->%PathMatchesStream_same_if_match_same_aux ->%PathMatchesStream_same_if_match_same_aux.
Qed.

    I don't know if this will still be enough for the refinements that you have in mind, though...