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?
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.
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.
Also the first match
is useless as it only renames a
and b
to c1
and x1
respectively.
Thanks for correction.
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 ...
)
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".
Is or
of return type bool
? I guess not and you meant orb
?
orb
You wrote or
.
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?
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: Oct 13 2024 at 01:02 UTC