## Stream: Coq users

### Topic: maximum element of list

#### zohaze (Aug 11 2021 at 16:11):

I want to write a lemma(g_function) which combines list_max l & mathematical function (gcd).

``````Fixpoint fun1 (l : list nat) :=
match l with
| nil => 1
| b::nil=> b
| b::t => gcd b (fun1 t)
end.

Lemma g_function: forall (l : list nat),
l <> nil -> list_max l = 0-> fun1 l=0.
I want to apply Nat.gcd_diag to prove above lemma. I have proved following lemma also(Lemma list_max_0 l: list_max l = 0 ->
forall a, nth a l 0 = 0.Admitted.)
``````

#### Lessness (Aug 11 2021 at 21:22):

``````Require Import List Lia.

Fixpoint fun1 (l : list nat) :=
match l with
| nil => 1
| b::nil=> b
| b::t => Nat.gcd b (fun1 t)
end.

Theorem aux a b: max a b = 0 -> a = 0 /\ b = 0.
Proof.
intros. destruct a, b.
+ auto.
+ simpl in *. lia.
+ rewrite Max.max_comm in H. simpl in *. lia.
+ simpl in *. lia.
Qed.

Lemma g_function: forall (l : list nat), l <> nil -> list_max l = 0 -> fun1 l = 0.
Proof.
intros. induction l.
+ congruence.
+ clear H. simpl in *. pose proof (aux _ _ H0). destruct H.
rewrite H. destruct l.
- reflexivity.
- rewrite IHl.
* simpl in *. reflexivity.
* congruence.
* auto.
Qed.
``````

#### zohaze (Aug 12 2021 at 15:54):

Thank you. discriminate & congruence are equal commands? Please comment under what condition we apply- pose proof (aux _ _ H0)

#### Ali Caglayan (Aug 12 2021 at 15:58):

`pose proof` is like `assert`. It simply does a `pose` (i.e. a local definition), and then forgets the body (using `clearbody`). It ends up just being an extra assumption.

#### Lessness (Aug 13 2021 at 18:53):

As far as I know, `congruence` does and knows all `discriminate` can do and much more.

#### sara lee (Aug 14 2021 at 04:26):

(deleted)

Last updated: Jun 18 2024 at 09:02 UTC