## Stream: Coq users

### Topic: false case

#### zohaze (Feb 22 2023 at 14:53):

Function gives a list nat between two numbers and this list contains minimum two natural numbers. ( like)
Definition two_num (a b:nat) (l : list nat):list nat :=
1) To use above list as input argument of below function, i have defined local variable (Variable req: list nat.)
Definition add (v:nat) (req:list nat) : list nat := v :: req.
To use the output list locally ,i should use another variable for output list of add function, then write it as
Definition add (v:nat) (req:list nat) : des := v::req ((Variable des: list nat.). How i can check the values of local variable?
2) During induction s , i get case of [] list which is not possible here because l cannot be empty, it must contain two elements.How i can prove it wrong?

#### Laurent Théry (Feb 22 2023 at 17:13):

1) How i can check the values of local variable?

``````Definition foo (m n : nat) :=
let sum := m + n in
match sum with
| 0 => 0
| S n1 => n1
end .
``````

2) During induction s , i get case of [] list which is not possible here because l cannot be empty, it must contain two elements.How i can prove it wrong?

``````Lemma my_proof : forall s, 1 < length s -> ...
so that during the induction, the assumption `1 < length s` will be false when `s = []`
``````