The Coq mailing list

[Djamila Baroudi <baroudi.d7 AT gmail.com>]

thanks a lot.

2014-03-18 11:13 GMT+01:00 Beta Ziliani <beta AT mpi-sws.org>:

What I meant is that in pattern matching you can only refer to
constructors of the inductive type.  The following code works:

Inductive st :Set:= q0 | q1 |q2 .
Inductive acts:Set:=pred(p:nat)|event(e:bool).

Function trans (q:st)(x:acts) :list st :=
match q, x with

  | q0, pred 1 =>  cons q1 nil
  | q1, pred 2 =>  cons q0 nil
  | q1, event true =>  cons q2 nil

  | _,_ =>    nil (A:=_)
end.

On Tue, Mar 18, 2014 at 11:08 AM, Djamila Baroudi <baroudi.d7 AT gmail.com> wrote:
> hello, you mean that i should write for example this:
>  Inductive st :Set:= q0 | q1 |q2 .
>>>     Inductive acts:Set:=pred(p:nat)|event(e:bool).
>>>     Definition a :acts:=pred(1).
>>>     Definition b:acts:=pred(2).
>>>     Definition c:acts:=event(true).
>>>     Function trans (q:st)(x:acts) :list st :=
>>>     match q, x with
>>>       | q0, a =>  cons q1 nil
>>>       | q1, b =>  cons q0 nil
>>>       | q1, c =>  cons q2 nil
>>>       | _,_ =>    nil (A:=_)
>>>     end.
>
> but with this code i have always a same error.
> thanks for your informations.
>
>
> 2014-03-18 10:54 GMT+01:00 Beta Ziliani <beta AT mpi-sws.org>:
>>
>> Sorry, forgot to mention that Coq is treating a,b,c in each pattern
>> matching clause as variables, and this is why is giving you the error.
>>
>> On Tue, Mar 18, 2014 at 10:52 AM, Beta Ziliani <beta AT mpi-sws.org> wrote:
>> > Basically your definitions a, b, c of acts are not constructors for
>> > the inductive type acts, which is what Coq expects (as most languages)
>> > in the match.  Also, take into account that writing
>> >
>> > Definition a : acts.
>> >
>> > is opening a goal to fill: what is a?  Probably what you meant is
>> >
>> > Axiom a : acts.
>> >
>> > (but be careful with axioms!).
>> >
>> > Hope it helps,
>> > Beta
>> >
>> >
>> >
>> > On Tue, Mar 18, 2014 at 10:42 AM, Djamila Baroudi <baroudi.d7 AT gmail.com>
>> > wrote:
>> >> hello,
>> >> i have a problem with definition of an automaton, an error was shown
>> >> when i
>> >> create this code:
>> >>
>> >>
>> >>     (*automate*)
>> >>
>> >>     Record automaton :Type:=
>> >>     mk_auto {
>> >>        states : Set;
>> >>        actions :Set;
>> >>        initial : states;
>> >>        transitions : states -> actions -> list states
>> >>     }.
>> >>     (*States*)
>> >>     Inductive st :Set:= q0 | q1 |q2 .
>> >>     Inductive acts:Set:=pred(p:nat)|event(e:bool).
>> >>     Definition a :acts.
>> >>     Definition b:acts.
>> >>     Definition c:acts.
>> >>     Function trans (q:st)(x:acts) :list st :=
>> >>     match q, x with
>> >>       | q0, a =>  cons q1 nil
>> >>       | q1, b =>  cons q0 nil
>> >>       | q1, c =>  cons q2 nil
>> >>       | _,_ =>    nil (A:=_)
>> >>     end.
>> >> the error was:
>> >> Error: This clause is redundant. (underlined this clause " | q1, c =>
>> >> cons
>> >> q2 nil")
>> >>
>> >> Thanks.
>> >>
>> >> --
>> >>
>> >> Mlle Djamila Baroudi
>> >>
>> >> Faculté des Sciences Exactes et Informatique,
>> >>
>> >> Université de Mostaganem,
>> >>
>> >> 27000 Mostaganem, Algérie.
>> >>
>> >>
>
>
>
>
> --
>
> Mlle Djamila Baroudi
>
> Faculté des Sciences Exactes et Informatique,
>
> Université de Mostaganem,
>
> 27000 Mostaganem, Algérie.
>
>

--

Mlle Djamila Baroudi                           

Faculté des Sciences Exactes et Informatique,        

Université de Mostaganem,

27000 Mostaganem, Algérie.