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?

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?

your theorem should be

```
Lemma my_proof : forall s, 1 < length s -> ...
```

so that during the induction, the assumption `1 < length s`

will be false when `s = []`

```
```

Last updated: Oct 04 2023 at 22:01 UTC