The goal of this lecture note is to build an awareness of the directionality of our proofs: backward, i.e., from the final goal to the initial hypothesis, or forward, i.e., from the initial hypothesis to the final goal?
The natural directionality of proofs in tCPA is backward, i.e., from final goal to initial hypothesis. Here is a simple example:
Proposition modus_ponens_and_even_more :
forall A B C D : Prop,
A -> (A -> B) -> (B -> C) -> (C -> D) -> D.
Proof.
intros A B C D H_A H_A_implies_B H_B_implies_C H_C_implies_D.
We can proceed backward, i.e., from the goal towards the initial hypothesis:
apply H_C_implies_D.
apply H_B_implies_C.
apply H_A_implies_B.
apply H_A.
However, we can also proceed forward, i.e., from the initial hypothesis towards the goal:
Restart.
intros A B C D H_A H_A_implies_B H_B_implies_C H_C_implies_D.
(* forward, from the initial hypothesis: *)
assert (H_B := H_A_implies_B H_A).
assert (H_C := H_B_implies_C H_B).
Check (H_C_implies_D H_C).
exact (H_C_implies_D H_C).
Qed.
Does it make a difference? Witness Show Proof, each assert step has created a let-expression in the resulting proof tree.
The goal of the following exercise is to investigate whether, and if so how and why, this directionality could make a difference.
Prove the following proposition (1) backward, in a goal-directed way, and (2) forward, from the assumptions:
Proposition foo :
forall P Q R1 R2 : Prop,
P -> (P -> Q) -> (Q -> R1) /\ (Q -> R2) -> R1 /\ R2.
Prove the following proposition (1) by using the split tactic as early as possible, and (2) by using the split tactic as late as possible:
Proposition bar :
forall P1 P2 Q R1 R2 T1 T2 : Prop,
P1 -> (P1 -> P2) -> (P2 -> Q) -> (Q -> R1) -> (R1 -> T1) -> (Q -> R2) -> (R2 -> T2) -> T1 /\ T2.
Prove the following proposition (1) by using the split tactic as early as possible, and (2) by using the split tactic as late as possible:
Proposition baz :
forall P Q R T U1 U2 : Prop,
P -> (P -> Q) -> (Q -> R) -> (R -> T) -> (T -> U1) -> (T -> U2) -> U1 /\ U2.
Complete the proof of baz_dual_early:
Proposition baz_dual_early :
forall P1 P2 Q R T U : Prop,
(P1 \/ P2) -> (P1 -> Q) -> (P2 -> Q) -> (Q -> R) -> (R -> T) -> (T -> U) -> U.
Proof.
intros P1 P2 Q R T U.
intros H_P1_or_P2 H_P1_implies_Q H_P2_implies_Q H_Q_implies_R H_R_implies_T H_T_implies_U.
(* use "destruct H_P1_or_P2 as [H_P1 | H_P2]." as early as you can *)
Complete the proof of baz_dual_late:
Proposition baz_dual_late :
forall P1 P2 Q R T U : Prop,
(P1 \/ P2) -> (P1 -> Q) -> (P2 -> Q) -> (Q -> R) -> (R -> T) -> (T -> U) -> U.
Proof.
intros P1 P2 Q R T U.
intros H_P1_or_P2 H_P1_implies_Q H_P2_implies_Q H_Q_implies_R H_R_implies_T H_T_implies_U.
(* use "destruct H_P1_or_P2 as [H_P1 | H_P2]." as late as you can *)
Compare the two previous proofs.
Complete the following proof:
Proposition baz_dual_early_or_late :
forall P1 P2 Q R T U : Prop,
(P1 \/ P2) -> (P1 -> Q) -> (P2 -> Q) -> (Q -> R) -> (R -> T) -> (T -> U) -> U.
Proof.
intros P1 P2 Q R T U.
intros [H_P1 | H_P2] H_P1_implies_Q H_P2_implies_Q H_Q_implies_R H_R_implies_T H_T_implies_U.
What do you end up with? A proof close to that of Proposition baz_dual_early, or to that of Proposition baz_dual_late? What do you conclude?
How would you prove the following propositions? Forward or backward?:
Proposition ladidah :
forall P1 P2 P3 P4 Q R T U : Prop,
(P1 \/ P2) \/ (P3 \/ P4) -> (P1 -> Q) -> (P2 -> Q) -> (P3 -> Q) -> (P4 -> Q) -> (Q -> R) -> (R -> T) -> (T -> U) -> U.
Proposition toodeloo :
forall P Q R T U1 U2 U3 U4: Prop,
P -> (P -> Q) -> (Q -> R) -> (R -> T) -> (T -> U1) -> (T -> U2) -> (T -> U3) -> (T -> U4) -> (U1 /\ U2) /\ (U3 /\ U4).
How complex could the size of such proofs be (relative to the number of hypotheses about P1, P2, P3, etc. and to the number of conclusions U1, U2, U3, etc.)?
Alfrothul: Well, since proofs are programs, a similar duplication could also occur when we write programs.
Bong-sun: Let’s see. How about we implement a function of type bool -> ...? We would then have a disjunction on the left of an arrow.
Alfrothul: OK. In OCaml, that would be something like:
fun (b : bool) f g h -> f (g (h b))
Pablito: Let me try, let me try:
# fun (b : bool) f g h -> f (g (h b));;
- : bool -> ('a -> 'b) -> ('c -> 'a) -> (bool -> 'c) -> 'b = <fun>
#
Dana: Thanks, Pablito. Now remembering that b and if b then true else false are observationally equivalent, we can also write:
fun (b : bool) f g h -> f (g (h (if b
then true
else false)))
Pablito: Let me try again:
# fun (b : bool) f g h -> f (g (h (if b then true else false)));;
- : bool -> ('a -> 'b) -> ('c -> 'a) -> (bool -> 'c) -> 'b = <fun>
#
Anton: Right. Same type.
Bong-sun: Yup. Alternatively – and equivalently – we can also test b as soon as it is declared, which is kind of like the Light of Inductil, sort of, but for programming and without recursion:
fun (b : bool) -> if b
then fun f g h -> f (g (h true))
else fun f g h -> f (g (h false))
Pablito: Trying:
# fun (b : bool) -> if b then fun f g h -> f (g (h true)) else fun f g h -> f (g (h false));;
- : bool -> ('a -> 'b) -> ('c -> 'a) -> (bool -> 'c) -> 'b = <fun>
#
Anton: Same type again.
Alfrothul: All right! So if we have a sum on the left-hand side of an arrow and if we destructure it early, the context of its use is duplicated.
Bong-sun: And if we destructure it late, the context of its use is not duplicated. It’s the same elephant.
Pablito: What if the variable that has a sum type occurs several times?
Anton: The same amount of duplication, look:
# fun (b : bool) -> fun f -> f (b, b);;
- : bool -> (bool * bool -> 'a) -> 'a = <fun>
# fun (b : bool) -> fun f -> f ((if b then true else false), (if b then true else false));;
- : bool -> (bool * bool -> 'a) -> 'a = <fun>
# fun (b : bool) -> if b then (fun f -> f (true, true)) else (fun f -> f (false, false));;
- : bool -> (bool * bool -> 'a) -> 'a = <fun>
#
Alfrothul: But then if the conditional expression is in a test...
Dana: Right. Here is one such expression, given the expressions e1, e2, e3, e4, and e5:
if (if e1
then e2
else e3)
then e4
else e5
Alfrothul: And here is an observationally equivalent expression without this nesting:
if e1
then if e2
then e4
else e5
then if e3
then e4
else e5
Bong-sun: Wow, e4 and e5 are duplicated.
Mimer: Here is the symmetric case where there is a conjunction in the conclusion. The type counterpart of a conjunction is a pair, so we shall need the two projection operators:
# fst;;
- : 'a * 'b -> 'a = <fun>
# fst (1, true);;
- : int = 1
# snd;;
- : 'a * 'b -> 'b = <fun>
# snd (1, true);;
- : bool = true
#
Mimer (continuing): The following property is named “surjective pairing”: given any expression e of type 'a * 'b, the expressions e and (fst e, snd e) are observationally equivalent in a pure and total language – or just in a language that uses call by name or call by need.
Dana: Right. The two occurrences of e in (fst e, snd e) mean that e is evaluated twice, and so if this evaluation emits a trace, for example, this trace would be duplicated. But if the language is pure and total, the two expressions behave the same.
Alfrothul: Right. And e is duplicated in (fst e, snd e), point well taken, thanks.
Created [09 Feb 2024]