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.
Last updated: Jan 31 2023 at 14:03 UTC