## Stream: Coq users

### Topic: error in writing

#### zohaze (Jan 07 2022 at 15:40):

``````Fixpoint eq (a b n1 n2: nat):bool:=
match a, b  with
c1 , x1 => match c1 with
| 0 => match x1 with
Z (d) =>  if leb d n1 then true else false
| 1 => match x1 with
Z (d')=> if leb d' n2 then true else false
end
end
end.
``````

Three time end is use for each case of c1?

#### Li-yao (Jan 07 2022 at 15:42):

You need to close a match before starting the next case of a match above it

``````Fixpoint eq (a b n1 n2: nat):bool:=
match a, b  with
c1 , x1 => match c1 with
| 0 => match x1 with
Z (d) =>  if leb d n1 then true else false
end
| 1 => match x1 with
Z (d')=> if leb d' n2 then true else false
end
end
end.
``````

#### Théo Winterhalter (Jan 07 2022 at 15:42):

You should indent your code properly. A `match` expression in Coq must always be concluded by an `end` (unlike in ocaml for instance).

``````Fixpoint eq (a b n1 n2 : nat) : bool :=
match a, b  with
| c1 , x1 =>
match c1 with
| 0 =>
match x1 with
| Z d => if leb d n1 then true else false
end
| 1 =>
match x1 with
| Z d' => if leb d' n2 then true else false
end
end
end.
``````

#### Théo Winterhalter (Jan 07 2022 at 15:43):

Also the first `match` is useless as it only renames `a` and `b` to `c1` and `x1` respectively.

#### zohaze (Jan 07 2022 at 15:51):

Thanks for correction.

#### Karl Palmskog (Jan 07 2022 at 15:52):

I also use Théo's style of indenting `match`, but it's not universal in the Coq community. (e.g., MathComp favors one-liners with a special notation `if c1 is 0 then ...`)

#### zohaze (Jan 07 2022 at 16:26):

``````Fixpoint eq (a b n1 n2 : nat) : bool :=
match a, b  with
| c1 , x1 =>
match c1 with
| 0 =>
match x1 with
| Z d =>  or (leb d n1)(leb d n2)
end
| 1 =>
match x1 with
| Z d' => or (leb d' n2) (leb d' n1)
end
end
end.
``````

Return type is still bool then why I get message " it is expected to have type "Prop".

#### Théo Winterhalter (Jan 07 2022 at 16:26):

Is `or` of return type `bool`? I guess not and you meant `orb`?

orb

#### Théo Winterhalter (Jan 07 2022 at 16:27):

You wrote `or`.

#### zohaze (Jan 07 2022 at 16:28):

Ok ,ok thank you. If I write any lemma which explain the behavior of above function ,then I have to write first whether c=0 or 1 then write second parameter then any output. Can you write any lemma about above?

#### Pierre Castéran (Jan 08 2022 at 08:18):

I don't understand what is `Z`in your code. Is it a typo for `S`?.
Or did you load any library (it would be useful to tell which one, or include your declaration of `Z` in the code you send.

Let's assume it's a typo (perhaps you should have sent us an exact copy of your example).

``````Notation Z := S.

Fixpoint eq (a b n1 n2 : nat) : bool :=
match a, b  with
| c1 , x1 =>
match c1 with
| 0 =>
match x1 with
| Z d =>  orb (leb d n1)(leb d n2)
end
| 1 =>
match x1 with
| Z d' => orb (leb d' n2) (leb d' n1)
end
end
end.
(*
Error: Non exhaustive pattern-matching: no clause found for pattern 0
*)
``````

In Coq, pattern-matchings should be exhaustive, which is not the case of your `match x1`.
You should add a clause `0 => ...` to both of your pattern-matching.

I'm not sure to answer your last question, but a typical exhaustive, non-ambiguous pattern-matching on `nat` can be as follows:

``````Fixpoint f (n:nat) : nat :=
match n with
0 => 33
| 1 => 42
| S (S p) => f p
end.
``````

Last updated: Sep 23 2023 at 13:01 UTC