Stream: Coq users

Topic: maximum element of list


view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Lessness (Aug 13 2021 at 18:53):

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

view this post on Zulip sara lee (Aug 14 2021 at 04:26):

(deleted)


Last updated: Jan 31 2023 at 14:03 UTC