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 ?

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`

).

```
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).

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.

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.

Is it an induction on `n`

? But `n`

does not occur in the right hand side of the implication, which depends only on `z`

and `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.

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: Jun 14 2024 at 19:02 UTC