PRFA.review4

Require Import List.
Import ListNotations.

Lemma in_add_right: ∀ A (x : A) l r,
    In x l →
    In x (l++r).
Proof.
Admitted.

Lemma in_add_left: ∀ A (x : A) l r,
    In x r →
    In x (l++r).
Admitted.

Hint Resolve in_add_right in_add_left: indb.

Lemma in_cons : ∀ A (x : A) y l,
    In x l →
    In x (y :: l).
Proof.
  simpl. auto.
Qed.

Hint Resolve in_cons : indb.

Goal ∀ A (x a b c d : A) l l',
    In x l →
    In x ([ a ; b ; c ] ++ l' ++ d :: l).
Proof.
  auto 7 with indb.
Qed.

(* Self-evaluation

1) Define a product type prod' : Type -> Type -> Type using records.
2) Prove that forall A B, prod' A B <-> A * B using a proof script or a proof term.
3) Give the type of an induction principle for prod'
4) Prove the induction principle with a proof script or a proof term.

*)

Record prod' A B :=
  {
    fst' : A ;
    snd' : B
  }.

Goal ∀ A B, (prod' A B → A × B) × (A × B → prod' A B).
Proof.
  intros A B. split.
  - intros [a b]. split; assumption.
  - intros [a b]. split; assumption.
Qed.

Goal ∀ A B, (prod' A B → A × B) × (A × B → prod' A B).
Proof.
  refine
  (fun A B : Type ⇒
     (fun p' : prod' A B ⇒
        match p' with
        | {| fst' := a; snd' := b |} ⇒ (a,b)
        end,
      fun p : A × B ⇒ let (a, b) := p in {| fst' := a; snd' := b |})).
Qed.

Definition prod'_ind : ∀ A B (P : prod' A B → Prop),
    (∀ a b, P ({| fst' := a ; snd' := b |}))
    → ∀ p, P p :=
  fun A B P h p ⇒
    match p with
    | {| fst' := a ; snd' := b |} ⇒ h a b
    end.