coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.