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.)
```

```
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.
```

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

`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.

As far as I know, `congruence`

does and knows all `discriminate`

can do and much more.

(deleted)

Last updated: Jun 18 2024 at 09:02 UTC