Stream: Coq users

Topic: error in writing


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip zohaze (Jan 07 2022 at 15:51):

Thanks for correction.

view this post on Zulip 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 ...)

view this post on Zulip 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".

view this post on Zulip Théo Winterhalter (Jan 07 2022 at 16:26):

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

view this post on Zulip zohaze (Jan 07 2022 at 16:27):

orb

view this post on Zulip Théo Winterhalter (Jan 07 2022 at 16:27):

You wrote or.

view this post on Zulip 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?

view this post on Zulip Pierre Castéran (Jan 08 2022 at 08:18):

I don't understand what is Zin 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: Feb 01 2023 at 11:04 UTC