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?

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