PRFA.review7

Require Import Lia.

Fixpoint add' (n m : nat) {struct m} :=
  match m with
  | 0 ⇒ n
  | S m' ⇒ S (add' n m')
  end.

Lemma add'_correct n m : add' n m = n + m.
Proof.
  (* fill in the full proof *)
  induction m.
  - simpl. lia.
  - simpl. rewrite IHm. lia.
Qed.

(* prove symmetry for leibniz equality with a proof term, i.e. prove *)
Definition leibniz_sym : ∀ A (x y : A),
    (∀ P : A → Prop, P x → P y) → (∀ Q : A → Prop, Q y → Q x) :=
  fun A x y e Q ⇒ e (fun z ⇒ Q z → Q x) (fun a ⇒ a).

Check eq_ind : ∀ (A : Type) (x : A) (P : A → Prop), P x → ∀ y : A, x = y → P y.

(* prove congruence for equality using eq_ind, i.e. prove the following *)
Definition f_equal {A B} (f : A → B) {u v} (e : u = v) : f u = f v :=
  eq_ind u (fun x ⇒ f u = f x) eq_refl v e.