пример индуктивного доказательства

NatComm.v

Require Import Nat.

Theorem add_comm: forall n m: nat, n + m = m + n.
Proof.
  induction n as [|n' IH].
  - (** n = O *)
    intro m. simpl. rewrite <- plus_n_O. reflexivity.
  - (** n = S n' *)
    intro m. simpl. rewrite <- plus_n_Sm. rewrite IH. reflexivity.
Qed.

Theorem add_comm': forall n m: nat, n + m = m + n.
Proof.
  induction n as [|n' IH].
  { (** n = O *)
    
    (* goal: forall m : nat, 0 + m = m + 0 *)
    
    intro m.
    (* context: m : nat *)
    (* ============================ *)
    (* goal: 0 + m = m + 0 *)
    
    simpl.
    (* m : nat *)
    (* ============================ *)
    (* m = m + 0 *)
    
    Check plus_n_O. (* plus_n_O: forall n : nat, n = n + 0 *)
    
    rewrite <- plus_n_O.
    (* m : nat *)
    (* ============================ *)
    (* m = m *)
    
    reflexivity. }

  (** n = S n' *)
  
  (* n' : nat *)
  (* IH : forall m : nat, n' + m = m + n' *)
  (* ============================ *)
  (* forall m : nat, S n' + m = m + S n' *)
  
  intro m.
  (* n' : nat *)
  (* IH : forall m : nat, n' + m = m + n' *)
  (* m : nat *)
  (* ============================ *)
  (* S n' + m = m + S n' *)
  
  simpl.
  (* n' : nat *)
  (* IH : forall m : nat, n' + m = m + n' *)
  (* m : nat *)
  (* ============================ *)
  (* S (n' + m) = m + S n' *)
  
  Check plus_n_Sm. (* plus_n_Sm: forall n m : nat, S (n + m) = n + S m *)
  
  rewrite <- plus_n_Sm.
  (* n' : nat *)
  (* IH : forall m : nat, n' + m = m + n' *)
  (* m : nat *)
  (* ============================ *)
  (* S (n' + m) = S (m + n') *)
  
  rewrite IH. (* применяем гипотезу индукции *)
  (* n' : nat *)
  (* IH : forall m : nat, n' + m = m + n' *)
  (* m : nat *)
  (* ============================ *)
  (* S (m + n') = S (m + n') *)
  
  reflexivity.
Qed.