(** TP09: Pigeons infinis *)
(*
TD outline:
- Reflexivity in Coq
- Infinite Pigeonhole Principle
*)
(******************************)
(** * Proofs by reflection **)
(******************************)
(** ** Computation in Coq **)
(** Computing in Coq means doing one of the following four reductions:
- beta : apply a function to its arguments
- iota : pattern matching related reduction
- delta : unfold a definition
(something defined by Definition, Fixpoint etc.)
- zeta : unfold a local definition
(something defined by [let ... := ... in])
The Coq tactics [cbv reduction_name] and [lazy reduction_name]
provoke normalisation of the goal with respect to the reduction in
parameter using a call-by-value and lazy strategy respectively.
The tactic [simpl] performs βι-reductions plus some δ-reductions
(only when further βι-reductions are possible). **)
(** 1) Observe the behaviour of the four reductions on the following
examples. **)
Check (1 + 2).
Eval cbv beta in (1 + 2).
Eval cbv delta in (1 + 2).
Eval cbv beta delta in (1 + 2).
Eval cbv delta iota in (1 + 2).
Eval cbv beta delta iota in (1 + 2).
Check ((fun x y => x + y) 1 ).
Eval cbv beta in ((fun x y => x + y) 1).
Eval cbv iota in (match 1 with 0 => false | S _ => true end).
Eval cbv iota beta in (match 1 with 0 => false | S _ => true end).
Eval cbv beta in (let f := (fun x y => x + y) in f 1).
Eval cbv delta in (let f := (fun x y => x + y) in f 1).
Eval cbv zeta in (let f := (fun x y => x + y) in f 1).
Eval cbv beta delta iota zeta in (let f := (fun x y => x + y) in f 1).
Eval compute in (let f := (fun x y => x + y) in f 1).
(** Some remarks:
- the tactic [compute] is equivalent to [cbv beta delta iota zeta].
- for the δ-reduction you can specify the definitions that are to be
unfolded or the ones that are not to be unfolded.
- [cbv], [lazy] and [compute] can be called on any goal in order to
normalise it. **)
(** Now, we will see the interest of using computation in proofs.
2) Prove the following lemma without automatic tactics. **)
Lemma le10_20 : 10 <= 20.
Proof.
repeat constructor.
Qed.
Print le10_20.
(** We can see that the size of the proof is proportional to the numbers.
Yet, informally, we would do this proof by computing if [le] was a
function. Now comes in handy the [leb] function! **)
Require Import Arith.Compare_dec.
Print leb.
SearchAbout leb.
Check leb_correct.
Check leb_complete.
(** 3) Prove the same lemma by computation, using [leb]. **)
Lemma leb10_20 : 10 <= 20.
Proof.
apply leb_complete.
reflexivity.
Qed.
(** We can see now that this last proof is of constant size, no matter how
large its inputs are. **)
Print leb10_20.
Print le10_20.
(** ** Associativity by reflection **)
(** To show that two expressions are equal modulo associativity of natural
number addition, we can do a proof by rewriting. **)
Require Import Arith.
Example reflection_test1 :
forall x y z t u, x + (y + z + (t + u)) = x + y + (z + (t + u)).
Proof. intros. repeat rewrite plus_assoc. reflexivity. Qed.
Print reflection_test1.
(** The size of the proof term grows with the number of rewrites needed
to "normalize" the terms w.r.t. associativity.
Our goal is to replace rewriting by reductions, which are more
efficient and do not appear in the proof terms.
The idea is to find a datatype that will represent the terms you want
to deal with (here, formulas with addition) such that you can replace
formal manipulation of the terms (like rewriting) with computation on
the new datatype.
1) What is a good datatype to represent expressions involving
additions? Define this datatype as an inductive type [repr]. **)
(** 2) Write the interpretation function [interp : repr -> nat] that
translates a term of the type [repr] to an expression of type
[nat] containing additions. **)
(** 3) Write the function [normal_assoc : repr -> repr] that performs the
equivalent of "normalisation w.r.t. associativity" on the new type
[repr]. (this is the computation that will replace rewriting) **)
(** 4) Show the lemmas
[[
repr_valid : forall t : repr, interp t = interp (normal_assoc t)
]]
and
[[
repr_valid_2 : forall t₁ t₂ : repr,
interp (normal_assoc t₁) = interp (normal_assoc t₂) ->
interp t₁ = interp t₂
]]
. **)
(** 5) Do an example proof of associativity of natural number addition by
moving to [repr] and reducing the corresponding terms. **)
Example reflection_test2 :
forall x y z t u, x + (y + z + (t + u)) = x + y + (z + (t + u)).
Proof.
...
Qed.
(** Infinite pigeonhole principle *)
(* Statement. If X is an infinite set which is the union of a finite number of X_i, then one of the X_i is infinite *)
(* Question 1. Write the proof on paper using classical logic *)
(* Question 2. Prove it in Coq *)
Definition infinite (P : nat -> Prop) := forall x, exists y, x < y /\ P y.
Section IPP.
Hypothesis Absurd : forall A, (~ ~ A) -> A.
Variable X : nat -> Prop.
Hypothesis Xu : infinite X.
Variable A : nat -> nat -> Prop.
Variable k : nat.
Hypothesis Xcovered : forall x, X x -> exists i, i <= k /\ A i x.
(* vous aurez peut-être besoin de quelques lemmes. *)
Theorem IPP : exists i, i <= k /\ infinite (A i).
Proof.
Admitted.
End IPP.
(* If you make it to the end, you can have a look at
td9.phis.me/Girard-Hukens.v
*)