Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Question about an eauto failure

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Question about an eauto failure


Chronological Thread 
  • From: Daniel Schepler <dschepler AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Question about an eauto failure
  • Date: Fri, 29 Nov 2013 13:03:39 -0800

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



  • [Coq-Club] Question about an eauto failure, Daniel Schepler, 11/29/2013

Archive powered by MHonArc 2.6.18.

Top of Page