Stream: Coq users

Topic: pattern matching

view this post on Zulip pianke (Sep 08 2023 at 16:24):

I have three natural numbers tot , a , b and nat list l. Such that tot = a x b.
H: tot > 0
H1: a = 1
H2: 1 < b
f (a b tot l)
matching tot
recursively call f (a b tot' l).
Since pattern matching is based on number(tot). Therefore, I want to write tot in terms of equality (tot=2,tot=3...). In above case tot <=2 . How i can use it in pattern matching or some othere way to solve it?

view this post on Zulip k32 (Sep 08 2023 at 17:45):

I am not sure I understood your question correctly, but comparison of Peano numbers is decidable, therefore you can apply this lemma to a pair of numbers, for example, and it will return a term that you can destruct, obtaining three branches where a < b, a = b, and a > b.

view this post on Zulip k32 (Sep 08 2023 at 18:35):

Or was it a question about creating a hypothesis of type tot = n while doing recursion on tot? This can be done via extended pattern matching:

Fixpoint f tot  :=
  match tot as n return tot = n -> True with
  | 0   => fun (Htot : tot = 0) => < something...>
  | S n => (fun (n0 : nat) (Htot : tot = S n0)  => <...> f n0) n
  end (eq_refl tot).

Or, more conveniently, like this:

Fixpoint foo (tot : nat) : <return type>.
  remember tot as n.
  destruct n.
  - exact (do_something).
  - ...

Sorry, it isn't clear to me what you're trying to achieve.

view this post on Zulip pianke (Sep 10 2023 at 16:47):

Q1) By using H1 and H2 ,how i can define tot according to definition(tot = axb)
Q2) I want to define tot in such a way that i can perform pattern matching on it and decrease it on each recursive call.
Want to creating a hypothesis of type tot = n from existing hypothesis.

view this post on Zulip k32 (Sep 10 2023 at 21:26):

Ok, I think my second message does pretty much what you want. The idea is that we treat tot as a regular Peano nat, so it's possible to do pattern-matching on it as usual, but in addition we create a hypothesis Htot : tot = <n>. Obviously, recursion will eventually reach the cases when Htot : tot = 1 and Htot : tot = 0, but if you have hypothesis of type tot > 2 in the context, then you can discharge these cases by contradiction.

view this post on Zulip Pierre Castéran (Sep 11 2023 at 06:37):

I'm not sure I understand the original post.

The problem with too informally stated questions is that we lack necessary information to give an appropriate answer.

That's the reason why we ask for re-playable scripts (a.k.a. minimal working examples) in Coq forums
(please look at this paragraph of Coq's code of conduct ).

If you quote the script you are working on (or send a gist link), we could discuss on the best way to declare your variables and define the function f.

Last updated: Jun 22 2024 at 16:02 UTC