The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

In the example below, eauto is failing to find proofs for some reason that I 
can't decipher.  But if I uncomment the definitions and hints for 
state_accepts_step_no_consume_rev and state_accepts_step_consume_rev, which 
just trivially reorder the arguments of the existing constructors, then the 
proof script works fine.  Any idea why that might be so?  (This is with 
Debian 
coq 8.4pl2dfsg-1.)

Record AbstractNDA (alphabet : Type) : Type := {
  states : Type;
  init_state : states;
  accepting_state : states;
  can_transition : states -> option alphabet -> states -> Prop
}.

Arguments states [alphabet] a.
Arguments init_state [alphabet] a.
Arguments accepting_state [alphabet] a.
Arguments can_transition [alphabet] a s1 c s2.

Section AbstractNDA_accepts.

Variables (alphabet : Type) (anda : AbstractNDA alphabet).

Inductive state_accepts : anda.(states) -> list alphabet -> Prop :=
| accepting_state_accepts_empty : state_accepts anda.(accepting_state) nil
| state_accepts_step_no_consume (s1 s2 : anda.(states)) (l : list alphabet) :
  anda.(can_transition) s1 None s2 -> state_accepts s2 l -> state_accepts s1 l
| state_accepts_step_consume (s1 s2 : anda.(states)) (c : alphabet)
  (l : list alphabet) :
    anda.(can_transition) s1 (Some c) s2 ->
    state_accepts s2 l ->
    state_accepts s1 (c :: l).

(*
Lemma state_accepts_step_no_consume_rev s1 s2 l :
  state_accepts s2 l -> anda.(can_transition) s1 None s2 ->
  state_accepts s1 l.
Proof.
eauto using state_accepts_step_no_consume.
Qed.

Lemma state_accepts_step_consume_rev s1 s2 c l :
  state_accepts s2 l -> anda.(can_transition) s1 (Some c) s2 ->
  state_accepts s1 (c :: l).
Proof.
eauto using state_accepts_step_consume.
Qed.
*)

Definition accepts (l : list alphabet) : Prop :=
  state_accepts anda.(init_state) l.

End AbstractNDA_accepts.

Arguments state_accepts [alphabet] anda s l.
Arguments accepts [alphabet] anda l.

Hint Constructors state_accepts : anda.
(*
Hint Extern 5 (state_accepts _ _ _) =>
  eapply state_accepts_step_no_consume_rev : anda.
Hint Extern 5 (state_accepts _ _ _) =>
  eapply state_accepts_step_consume_rev : anda.
*)

Section AbstractNDA_concat.

Variables (alphabet : Type) (anda1 anda2 : AbstractNDA alphabet).

Inductive anda_concat_can_transition :
  (anda1.(states) + anda2.(states)) -> option alphabet ->
  (anda1.(states) + anda2.(states)) -> Prop :=
| can_transition_left : forall (s1 s2 : anda1.(states)) (c : option alphabet),
  anda1.(can_transition) s1 c s2 ->
  anda_concat_can_transition (inl s1) c (inl s2)
| can_transition_right : forall (s1 s2 : anda2.(states)) (c : option 
alphabet),
  anda2.(can_transition) s1 c s2 ->
  anda_concat_can_transition (inr s1) c (inr s2)
| can_transition_cross : anda_concat_can_transition
                           (inl anda1.(accepting_state))
                           None
                           (inr anda2.(init_state)).

Hint Constructors anda_concat_can_transition : anda_concat.

Definition anda_concat : AbstractNDA alphabet := {|
  states := anda1.(states) + anda2.(states);
  init_state := inl anda1.(init_state);
  accepting_state := inr anda2.(accepting_state);
  can_transition := anda_concat_can_transition
|}.

Hint Extern 1 (can_transition anda_concat _ _ _) => do 2 red : anda_concat.

Inductive anda_concat_state_should_accept :
  anda1.(states) + anda2.(states) -> list alphabet -> Prop :=
| should_accept_right : forall (s : anda2.(states)) (l : list alphabet),
  anda2.(state_accepts) s l -> anda_concat_state_should_accept (inr s) l
| should_accept_left : forall (s : anda1.(states)) (l1 l2 : list alphabet),
  anda1.(state_accepts) s l1 -> anda2.(accepts) l2 ->
  anda_concat_state_should_accept (inl s) (l1 ++ l2).

Hint Constructors anda_concat_state_should_accept : anda_concat.

Lemma anda_concat_should_accept_impl_accepts_right :
  forall (s : anda2.(states)) (l : list alphabet),
  anda2.(state_accepts) s l -> anda_concat.(state_accepts) (inr s) l.
Proof.
induction 1;
try change (inr (accepting_state anda2)) with
  (accepting_state anda_concat);
eauto with anda anda_concat.
Qed.

End AbstractNDA_concat.
-- 
Daniel Schepler