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?
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
.
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) => <...do 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).
- ...
Defined.
Sorry, it isn't clear to me what you're trying to achieve.
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.
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.
I'm not sure I understand the original post.
In the context associated with the hypotheses, we can infer tot = b
, hence tot >= 2
(if I take the assertion tot = a x b
as an hypothesis to add to H
, H1
, H2
).
Is the inequality tot <= 2
another hypothesis (which would imply tot = 2
) or a typo ?
Does the argument l
of f
play a role in this issue?
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