rocq prover - Proving that Multiplication is distributive - Stack Overflow

I am trying to prove the following theorem from Software Foundations>Induction

I am using Coq 8.19.2

The beginning of my solution is as follows :

Theorem mult_plus_distr_r : forall n m p : nat,
  (n + m) * p = (n * p) + (m * p).
    (* c *)
Proof.
  (* FILL IN HERE *) 
  induction p as [|p' IHp'].
  rewrite mult_0_r.
  rewrite mult_0_r.
  rewrite mult_0_r.
  reflexivity.
Admitted.

I am stuck on this subgoal (n + m) * S p' = n * S p' + m * S p' I see that I have to rewrite (n + m) * S p' as (n + m) * p + (n + m)' and n * S p' + m * S pasn * p' + n + m * p' + m` but I don't exactly have this hypothesis in my premises.

I want to stick as much as possible to the manual and avoid using commands not introduced before, for exemple, auto or resorting to libraries.

So far I have proven the following :

Theorem plus_O_n : forall n : nat, 0 + n = n.
Theorem plus_O_n' : forall n : nat, 0 + n = n.
Theorem plus_O_n'' : forall n : nat, 0 + n = n.
Theorem plus_1_l : forall n:nat, 1 + n = S n.
Theorem mult_0_l : forall n:nat, 0 * n = 0.
Theorem andb_commutative : forall b c, andb b c = andb c b.
Theorem andb_commutative' : forall b c, andb b c = andb c b.
Theorem lower_grade_F_Minus : lower_grade (Grade F Minus) = (Grade F Minus).
Theorem eqb_refle : forall n : nat, (eqb n n) = true.
Theorem mult_1_l : forall n:nat, 1 * n = n.
Theorem plus_id_exercise : forall n m o : nat,
  n = m -> m = o -> n + m = m + o.
Theorem mult_n_0_m_0 : forall p q : nat,
  (p * 0) + (q * 0) = 0.
Theorem mult_n_1 : forall p : nat,
  p * 1 = p.
Theorem plus_1_neq_0_firsttry : forall n : nat,
  (n + 1) =? 0 = false.
Theorem plus_1_neq_0 : forall n : nat,
  (n + 1) =? 0 = false.
Theorem negb_involutive : forall b : bool,
  negb (negb b) = b.
Theorem andb3_exchange :
  forall b c d, andb (andb b c) d = andb (andb b d) c.
Theorem andb_true_elim2 : forall b c : bool,
  andb b c = true -> c = true.
Theorem plus_1_neq_0' : forall n : nat,
  (n + 1) =? 0 = false.
Theorem andb_commutative'' :
  forall b c, andb b c = andb c b.
Theorem zero_nbeq_plus_1 : forall n : nat,
  0 =? (n + 1) = false.
Theorem letter_comparison_Eq :
  forall l, letter_comparison l l = Eq.
Theorem lower_letter_lowers: forall (l : letter),
  letter_comparison (lower_letter l) l = Lt.
Theorem lower_letter_F_is_F:
  lower_letter F = F.
Theorem add_0_r_firsttry : forall n:nat,
  n + 0 = n.
Theorem add_0_r : forall n:nat,
  n + 0 = n.
Theorem mul_0_r : forall n:nat,
  n * 0 = 0.
Theorem plus_n_Sm : forall n m : nat,
  S (n + m) = n + (S m).
Theorem add_comm : forall n m : nat,
  n + m = m + n.
Theorem add_assoc : forall n m p : nat,
  n + (m + p) = (n + m) + p.
Theorem add_assoc2 : forall n m p : nat,
  n + (m + p) = n + m + p.
Theorem even_S : forall n : nat,
  even (S n) = negb (even n).
Theorem mult_0_plus' : forall n m : nat,
  (n + 0 + 0) * m = n * m.
Theorem plus_rearrange_firsttry : forall n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Theorem plus_rearrange : forall n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Theorem add_shuffle3 : forall n m p : nat,
  n + (m + p) = m + (n + p).
Theorem mult_0_r : forall n:nat,
  n * 0 = 0.
Theorem mul_comm : forall m n : nat,
  m * n = n * m.
Theorem plus_leb_compat_l : forall n m p : nat,
  n <=? m = true -> (p + n) <=? (p + m) = true.
Theorem leb_refl : forall n:nat,
  (n <=? n) = true.
Theorem zero_neqb_S : forall n:nat,
  0 =? (S n) = false.
Theorem andb_false_r : forall b : bool,
  andb b false = false.
Theorem S_neqb_0 : forall n:nat,
  (S n) =? 0 = false.
Theorem plus_id_example : forall n m:nat,
  n = m ->
  n + n = m + m.
Theorem identity_fn_applied_twice :
  forall (f : bool -> bool),
  (forall (x : bool), f x = x) ->
  forall (b : bool), f (f b) = b.
Theorem negation_fn_applied_twice  :
  forall (f : bool -> bool),
  (forall (x : bool), f x = negb x) ->
  forall (b : bool), f (f b) = b.
Theorem andb_eq_orb :
  forall (b c : bool),
  (andb b c = orb b c) ->
  b = c.
Theorem all3_spec : forall b c : bool,
  orb
    (andb b c)
    (orb (negb b)
         (negb c))
  = true.

I will go over these and think about how I can rewrite this or maybe change my induction hypothesis although I believe to be correct in this case.

I am trying to prove the following theorem from Software Foundations>Induction

I am using Coq 8.19.2

The beginning of my solution is as follows :

Theorem mult_plus_distr_r : forall n m p : nat,
  (n + m) * p = (n * p) + (m * p).
    (* c *)
Proof.
  (* FILL IN HERE *) 
  induction p as [|p' IHp'].
  rewrite mult_0_r.
  rewrite mult_0_r.
  rewrite mult_0_r.
  reflexivity.
Admitted.

I am stuck on this subgoal (n + m) * S p' = n * S p' + m * S p' I see that I have to rewrite (n + m) * S p' as (n + m) * p + (n + m)' and n * S p' + m * S pasn * p' + n + m * p' + m` but I don't exactly have this hypothesis in my premises.

I want to stick as much as possible to the manual and avoid using commands not introduced before, for exemple, auto or resorting to libraries.

So far I have proven the following :

Theorem plus_O_n : forall n : nat, 0 + n = n.
Theorem plus_O_n' : forall n : nat, 0 + n = n.
Theorem plus_O_n'' : forall n : nat, 0 + n = n.
Theorem plus_1_l : forall n:nat, 1 + n = S n.
Theorem mult_0_l : forall n:nat, 0 * n = 0.
Theorem andb_commutative : forall b c, andb b c = andb c b.
Theorem andb_commutative' : forall b c, andb b c = andb c b.
Theorem lower_grade_F_Minus : lower_grade (Grade F Minus) = (Grade F Minus).
Theorem eqb_refle : forall n : nat, (eqb n n) = true.
Theorem mult_1_l : forall n:nat, 1 * n = n.
Theorem plus_id_exercise : forall n m o : nat,
  n = m -> m = o -> n + m = m + o.
Theorem mult_n_0_m_0 : forall p q : nat,
  (p * 0) + (q * 0) = 0.
Theorem mult_n_1 : forall p : nat,
  p * 1 = p.
Theorem plus_1_neq_0_firsttry : forall n : nat,
  (n + 1) =? 0 = false.
Theorem plus_1_neq_0 : forall n : nat,
  (n + 1) =? 0 = false.
Theorem negb_involutive : forall b : bool,
  negb (negb b) = b.
Theorem andb3_exchange :
  forall b c d, andb (andb b c) d = andb (andb b d) c.
Theorem andb_true_elim2 : forall b c : bool,
  andb b c = true -> c = true.
Theorem plus_1_neq_0' : forall n : nat,
  (n + 1) =? 0 = false.
Theorem andb_commutative'' :
  forall b c, andb b c = andb c b.
Theorem zero_nbeq_plus_1 : forall n : nat,
  0 =? (n + 1) = false.
Theorem letter_comparison_Eq :
  forall l, letter_comparison l l = Eq.
Theorem lower_letter_lowers: forall (l : letter),
  letter_comparison (lower_letter l) l = Lt.
Theorem lower_letter_F_is_F:
  lower_letter F = F.
Theorem add_0_r_firsttry : forall n:nat,
  n + 0 = n.
Theorem add_0_r : forall n:nat,
  n + 0 = n.
Theorem mul_0_r : forall n:nat,
  n * 0 = 0.
Theorem plus_n_Sm : forall n m : nat,
  S (n + m) = n + (S m).
Theorem add_comm : forall n m : nat,
  n + m = m + n.
Theorem add_assoc : forall n m p : nat,
  n + (m + p) = (n + m) + p.
Theorem add_assoc2 : forall n m p : nat,
  n + (m + p) = n + m + p.
Theorem even_S : forall n : nat,
  even (S n) = negb (even n).
Theorem mult_0_plus' : forall n m : nat,
  (n + 0 + 0) * m = n * m.
Theorem plus_rearrange_firsttry : forall n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Theorem plus_rearrange : forall n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Theorem add_shuffle3 : forall n m p : nat,
  n + (m + p) = m + (n + p).
Theorem mult_0_r : forall n:nat,
  n * 0 = 0.
Theorem mul_comm : forall m n : nat,
  m * n = n * m.
Theorem plus_leb_compat_l : forall n m p : nat,
  n <=? m = true -> (p + n) <=? (p + m) = true.
Theorem leb_refl : forall n:nat,
  (n <=? n) = true.
Theorem zero_neqb_S : forall n:nat,
  0 =? (S n) = false.
Theorem andb_false_r : forall b : bool,
  andb b false = false.
Theorem S_neqb_0 : forall n:nat,
  (S n) =? 0 = false.
Theorem plus_id_example : forall n m:nat,
  n = m ->
  n + n = m + m.
Theorem identity_fn_applied_twice :
  forall (f : bool -> bool),
  (forall (x : bool), f x = x) ->
  forall (b : bool), f (f b) = b.
Theorem negation_fn_applied_twice  :
  forall (f : bool -> bool),
  (forall (x : bool), f x = negb x) ->
  forall (b : bool), f (f b) = b.
Theorem andb_eq_orb :
  forall (b c : bool),
  (andb b c = orb b c) ->
  b = c.
Theorem all3_spec : forall b c : bool,
  orb
    (andb b c)
    (orb (negb b)
         (negb c))
  = true.

I will go over these and think about how I can rewrite this or maybe change my induction hypothesis although I believe to be correct in this case.

• rocq-prover

Share Improve this question Follow asked Dec 31, 2024 at 12:26 user18476546user18476546 3

• 1 @JulioDiEgidio you can do induction without intros – Li-yao Xia Commented Dec 31, 2024 at 16:02
• 1 What do you mean? – Li-yao Xia Commented Dec 31, 2024 at 16:41
• 1 @Li-yaoXia Yes, sorry, I have had a hallucination: deleted. Anyway, for the OP: it can be proved by induction on p. Hint: there is a theorem forall n m : nat, n * m + n = n * S m in a library. – user22862809 Commented Dec 31, 2024 at 16:49

Add a comment  | 

1 Answer 1

Sorted by: Reset to default 1

If you print the definition of mult, you'll see that it is defined by a fixpoint on n and not on p, so you would rather like to do your induction on the left side of *. It turns out that addalso is defined on n so it will simplify nicely. It is then ok to prove.

Nat.mul =
fix mul (n m : nat) {struct n} : nat :=
match n with
| 0 => 0
| S p => m + mul p m
end      : nat -> nat -> nat  Arguments Nat.mul (n m)%nat_scope

If you really want to do it by induction on p, I suggest you first start by using bullets to make the code clearer. In the second case,

Theorem mult_plus_distr_r : forall n m p : nat,
  (n + m) * p = (n * p) + (m * p).
    (* c *)
Proof.
  induction p as [|p' IHp']; cbn.
 - admit.
 - (* stuck *)

I this case, you simplify the goal using the lemma you have proven, then use somehow the recursion hypothesis IHp' as you are in the recursive case. Then, you may need to manipulate a bit the goal after so it can be prove by reflexivity like using associativity or sth else.