1.证明下列三条性质

Theorem plus_n_Sm

Theorem plus_n_Sm : ∀ n m : nat,
S (n + m) = n + (S m).
Proof.
(* FILL IN HERE *) Admitted.

Coq代码

Theorem plus_n_Sm : forall n m : nat,
S (n + m) = n + (S m).
Proof.
intros n. induction n as [| n' IHn'].
- intros m. induction m as [| m' IHm'].
  -- simpl. reflexivity.
  -- simpl. reflexivity.
- intros m. induction m as [| m' IHm'].
  -- simpl. rewrite -> IHn'. reflexivity. 
  -- simpl. rewrite -> IHn'. reflexivity. Qed.

Theorem add_comm

Theorem add_comm : ∀ n m : nat,
n + m = m + n.
Proof.
(* FILL IN HERE *) Admitted.

Coq代码

Theorem add_comm : forall n m : nat,
n + m = m + n.
Proof.
induction n as [| n' IHn'].
- induction m as [| m' IHm'].
  -- simpl. reflexivity.
  -- simpl. rewrite <- IHm'. simpl. reflexivity.
- induction m as [| m' IHm']. 
  -- simpl. rewrite -> IHn'. simpl. reflexivity.
  -- simpl. rewrite <- IHm'. rewrite -> IHn'. simpl. rewrite -> IHn'. reflexivity.
Qed.

Theorem add_assoc

Theorem add_assoc : ∀ n m p : nat,
n + (m + p) = (n + m) + p.
Proof.
(* FILL IN HERE *) Admitted.

Coq代码

Theorem add_assoc : forall n m p : nat,
n + (m + p) = (n + m) + p.
Proof.
induction n as [| n' IHn'].
- induction m as [| m' IHm'].
  -- induction p as [| p' IHp'].
  	--- simpl. reflexivity.
  	--- simpl. reflexivity.
  -- induction p as [| p' IHp'].
  	--- simpl. reflexivity.
  	--- simpl. reflexivity.
- induction m as [| m' IHm'].
  -- simpl. induction p as [| p' IHp'].
  	--- rewrite <- IHn'. simpl. reflexivity.
  	--- rewrite <- IHn'. simpl. reflexivity.
  -- simpl. induction p as [| p' IHp'].
  	--- rewrite <- IHn'. simpl. reflexivity.
  	--- rewrite <- IHn'. simpl. reflexivity.
Qed.

2.

Example test_ht1 : ht 0 [] = (0,0).
Proof. reflexivity. Qed.
Example test_ht2 : ht 0 [3] = (3,3).
Proof. reflexivity. Qed.
Example test_ht3 : ht 0 [1;2;3;4] = (1,4).
Proof. reflexivity. Qed.

Coq代码

Inductive natprod : Type :=
  | pair (n1 n2 : nat).

Inductive natlist : Type :=
  | nil
  | cons (n : nat) (l : natlist).

Notation "( x , y )" := (pair x y).

Notation "x :: l" := (cons x l)
                   (at level 60, right associativity).

Fixpoint app (l1 l2 : natlist) : natlist :=
  match l1 with
  | nil    => l2
  | h :: t => h :: (app t l2)
  end.

Notation "x ++ y" := (app x y)
                     (right associativity, at level 60).

Notation "[ ]" := nil.

Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).

Fixpoint rev (l:natlist) : natlist :=
  match l with
  | nil => nil
  | h :: t => rev t ++ [h]
  end.

Definition hd (default : nat) (l : natlist) : nat :=
  match l with
  | nil => default
  | h :: t => h
  end.
(** 正文*)
Definition ht (default : nat) (l : natlist) : natprod :=
 (hd 0 l,hd 0 (rev l)).

Example test_ht1 : ht 0 [] = (0,0).
Proof. reflexivity. Qed.
Example test_ht2 : ht 0 [3] = (3,3).
Proof. reflexivity. Qed.
Example test_ht3 : ht 0 [1;2;3;4] = (1,4).
Proof. reflexivity. Qed.