sara lee (Jul 16 2022 at 17:09): sara lee (Jul 16 2022 at 17:09):I need n > 0 to solve the goal statement, but in hypothesis i have (S n)> 0. In this case what i should do or what modification i should made in hypothesis ?
Mukesh Tiwari (Jul 16 2022 at 21:08):You question does not have enough information to answer it precisely. Could you please post your theorem that you are trying to prove. Given that your goal demands 0 < n and you have 0 < S n in assumption, it is not provable because n can be 0 and your assumption holds but the goal is not provable (0 < 0).
sara lee (Jul 17 2022 at 08:27):H0: (S n)>0
H: n>0 ->
(length l > 0->
z < length l ->
count z l <= count 0 l)
goal: count z l <= S ( count 0 l)
I have n>0 in hypothesis(initially) ,but after induction it became (S n). To prove above i need n>0 but have (S n).
James Wood (Jul 19 2022 at 12:55):What does it look like before the induction? For the n > 0 assumption to remain as-is in the type of H seems a bit strange.
sara lee (Jul 26 2022 at 14:04):before induction it is n>0. I want to prove statement " if count of 0 is greater than count of z in l,then addition of another 0 will not effect the existing relation.
Pierre Castéran (Jul 26 2022 at 17:17):Is it an induction on n ? But ndoes not occur in the right hand side of the implication, which depends only on zand l. If I try to prove some proposition forall n, 0 < n -> Q, I obtain a similar goal.
May be it's worth trying an induction on l. But it's difficult to be more specific without the exact Coq script which led to this problem.
sara lee (Jul 30 2022 at 06:20):I have function f which is responsible for the addition of different elements in the output list after test condition.
Now have hypothesis that in the output list count of z is less or equal to 0. If test condition is satisfied and 0 is adding in the list
. Performed induction on l and destruct n (both). I want to know how i should proceed? Yes proving proposition.
Last updated: Oct 05 2023 at 02:01 UTC