# TP08: IPP & reflection

# The Infinite Pigeonhole Principle

∀ U : nat → Prop, UB U →

∀ (I : nat → nat → Prop) (k : nat),

(∀ x : nat, U x → ∃ i : nat, i ≤ k ∧ I i x) →

∃ i : nat, i ≤ k ∧ UB (fun t : nat => U t ∧ I i t)

Require Import Arith.

Require Import Max.

Require Import Omega.

Require Import Max.

Require Import Omega.

Unbounded sets

Let UB (I : nat -> Prop) : Prop := forall x, exists y, x <= y /\ I y.

First show that if ∀i ≤ k, ∃b, ∀x, I i x → x ≤ b, then
∃b, ∀i ≤ k, ∀x, I i x → x ≤ b.
This does not require classical logic.

Section MaxBounded.

Variable I : nat -> nat -> Prop.

Definition Bounded (k : nat) : Prop :=

forall i, i <= k -> exists b, forall x, I i x -> x <= b.

Definition Max (k : nat) : Prop :=

exists b, forall i, i <= k -> forall x, I i x -> x <= b.

Lemma Bounded_Imp_Max : forall k, Bounded k -> Max k.

Proof.

...

Qed.

End MaxBounded.

Section IPP.

Axiom DNE : forall P, ~~P -> P.

Variable U : nat -> Prop.

Hypothesis UBU : UB U.

Variable I : nat -> nat -> Prop.

Variable k : nat.

Hypothesis I_bounded : forall x, U x -> exists i, i <= k /\ I i x.

Theorem IPP : exists i, i <= k /\ UB (fun t => U t /\ I i t).

Proof.

...

Qed.

End IPP.

Variable I : nat -> nat -> Prop.

Definition Bounded (k : nat) : Prop :=

forall i, i <= k -> exists b, forall x, I i x -> x <= b.

Definition Max (k : nat) : Prop :=

exists b, forall i, i <= k -> forall x, I i x -> x <= b.

Lemma Bounded_Imp_Max : forall k, Bounded k -> Max k.

Proof.

...

Qed.

End MaxBounded.

Section IPP.

Axiom DNE : forall P, ~~P -> P.

Variable U : nat -> Prop.

Hypothesis UBU : UB U.

Variable I : nat -> nat -> Prop.

Variable k : nat.

Hypothesis I_bounded : forall x, U x -> exists i, i <= k /\ I i x.

Theorem IPP : exists i, i <= k /\ UB (fun t => U t /\ I i t).

Proof.

...

Qed.

End IPP.

# Proofs by reflection

## Computation in Coq

- 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)

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).

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:
Now, we will see the interest of using computation in proofs.
2) Prove the following lemma without automatic tactics.

- 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.

Lemma le10_20 : 10 <= 20.

Proof.

...

Qed.

Print le10_20.

Proof.

...

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.

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.

...

Qed.

Proof.

...

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.

Print le10_20.

## Associativity by reflection

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.

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 : ∀ t : repr, interp t = interp (normal_assoc t)
and

repr_valid_2 : ∀ 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.

repr_valid : ∀ t : repr, interp t = interp (normal_assoc t)

repr_valid_2 : ∀ t₁ t₂ : repr,

interp (normal_assoc t₁) = interp (normal_assoc t₁) →

interp t₁ = interp t₂

Example reflection_test2 :

forall x y z t u, x + (y + z + (t + u)) = x + y + (z + (t + u)).

Proof.

...

Qed.

forall x y z t u, x + (y + z + (t + u)) = x + y + (z + (t + u)).

Proof.

...

Qed.

It is annoying to have to manually insert interp in the goal and
guess which term will give the correct interpretation. We would like
to have a function doing it for us but that is impossible: you cannot
pattern match an expression of type nat to test wether it contains
+ because + is not a constructor.
The solution is to use the tactic language and perform pattern
matching there.
6) Write a tactic that does the work automatically (i.e. introduce
interp, then apply repr_valid_2) and test it.

Ltac nat_to_repr n := ...

Ltac rassoc := ...

Example reflection_test3 :

forall x y z t u, x + (y + z + (t + u)) = x + y + (z + (t + u)).

Proof. intros. rassoc. Qed.

Ltac rassoc := ...

Example reflection_test3 :

forall x y z t u, x + (y + z + (t + u)) = x + y + (z + (t + u)).

Proof. intros. rassoc. Qed.

7) Generalize your work for an arbitrary type A with an arbitrary
operation op that is associative.

Parameters (A : Set) (op : A -> A -> A)

(assoc : forall x y z, op x (op y z) = op (op x y) z).

(assoc : forall x y z, op x (op y z) = op (op x y) z).

8) Adapt the previous work to the case where op has a neutral
element to the right and to the left.

Parameters (zero: A)

(zero_l : forall (x : A), op zero x = x)

(zero_r : forall (x : A), op x zero = x).

(zero_l : forall (x : A), op zero x = x)

(zero_r : forall (x : A), op x zero = x).

9) How would you deal with equalities modulo associativity and
commutativity?
Write the corresponding datastructures, lemmas and tactics.
Remark: this technology is used in the implementation of the automatic
tactics ring and field.

This page has been generated by coqdoc