Stream: Coq users

Topic: length l

view this post on Zulip sara lee (Jan 18 2022 at 14:56):

I have natural number list whose length is not zero ,but 1 mod length l is zero. It means length l is one because only 1 mod 1=0. Can i write this?
(length l) <> 0 ->
0= 1 mod (length l)->
(length l)=1.

view this post on Zulip Michael Soegtrop (Jan 18 2022 at 17:08):

Yes, this is provable (for any nat) as follows:

Require Import PeanoNat.

Lemma Test: forall (n : nat), n <> 0 -> 0 = 1 mod n -> n=1.
Proof.
  intros n Hnz Hmod.
  destruct n.
  1: destruct Hnz; reflexivity.
  Search (_ mod _ = 0).
  pose proof Nat.mod_divides 1 (S n) Hnz as H.
  destruct H as [H _].
  specialize (H (eq_sym Hmod)).
  destruct H.
  symmetry in H.
  Search(?a * ?b = 1).
  apply Nat.mul_eq_1 in H.
  tauto.
Qed.

Last updated: Oct 01 2023 at 18:01 UTC