conj_fact

conj_fact.v

(** **** Exercise: 2 stars, optional (conj_fact) *)
(** Construct a proof object demonstrating the following proposition. *)

Theorem conj_fact : forall P Q R, P /\ Q -> Q /\ R -> P /\ R.
Proof.
  intros P Q R HPQ HQR.
  apply conj.
  (* Case "left". *)
    inversion HPQ as [HP HQ].
    apply HP.
  (* Case "right". *)
    inversion HQR as [HQ HR].
    apply HR.
Qed.
(* Print conj_fact. *)

Definition conj_fact : forall P Q R, P /\ Q -> Q /\ R -> P /\ R :=
(* This is the output of the above [Print], which is not accepted by Coq. *)
fun (P Q R : Prop) (HPQ : P /\ Q) (HQR : Q /\ R) =>
conj P R
  ((fun H : P => H)
     match HPQ with
     | conj HP HQ => (fun (HP0 : P) (_ : Q) => HP0) HP HQ
     end)
  ((fun H : R => H)
     match HQR with
     | conj HQ HR => (fun (_ : Q) (HR0 : R) => HR0) HQ HR
     end)
     : forall P Q R : Prop, P /\ Q -> Q /\ R -> P /\ R.

Error:

Toplevel input, characters 119-398:
Error: In environment
P : Prop
Q : Prop
R : Prop
HPQ : P /\ Q
HQR : Q /\ R
The term
 "conj P R
    ((fun H : P => H)
       match HPQ with
       | conj HP HQ => (fun (HP0 : P) (_ : Q) => HP0) HP HQ
       end)
    ((fun H : R => H)
       match HQR with
       | conj HQ HR => (fun (_ : Q) (HR0 : R) => HR0) HQ HR
       end)" has type "P /\ R" while it is expected to have type
 "forall P Q R : Prop, P /\ Q -> Q /\ R -> P /\ R".

The solution is to parenthesize everything between := and : forall.

With beta-reduction, the generated output can be simplified to

Definition conj_fact : forall P Q R, P /\ Q -> Q /\ R -> P /\ R :=
  ( fun (P Q R : Prop) (HPQ : P /\ Q) (HQR : Q /\ R) =>
      conj P R
           ((fun H : P => H)
              match HPQ with
                | conj HP HQ => HP
              end)
           ((fun H : R => H)
              match HQR with
                | conj HQ HR => HR
              end)
  ) : forall P Q R : Prop, P /\ Q -> Q /\ R -> P /\ R.