Library BoundedNat.even_half

Author: Jean-François Monin, Verimag, Université Grenoble Alpes

Beginner example: even natural numbers their half (without distraction by irrelevant odd numbers).

Here there are NO bounded natural numbers, only usual natural numbers. The main points to be illustrated here are:

computing the half using the Braga method without graph
definition of half using even_inv + partial correctness
proofs of half_pirr and even_unique using even_inv
definition of even_rect using even_inv_π = combination small inversion + projection
standard inversion already fails in various ways

This example is anyway a good warming up for bounded natural numbers.

Require Import Utf8.

Definition of even and its small inversion

Inductive even : ∀ n , Prop :=
| Ev0 : even 0
| Ev2 n : even n → even (S (S n)).

Small inversion

Inductive is_Ev0 : even 0 → Prop :=
   | is_Ev0_intro : is_Ev0 Ev0.
Inductive no_Ev1 : even 1 → Prop :=.
Inductive is_Ev2 n : even (S (S n)) → Prop :=
   | is_Ev2_intro (e : even n) : is_Ev2 n (Ev2 n e).

Definition even_inv {n} (e : even n) :
    match n return even n → Prop with
    | 0 ⇒ is_Ev0
    | 1 ⇒ no_Ev1
    | S (S n) ⇒ is_Ev2 n
    end e.
Proof. destruct e; constructor. Defined.

Lemma even_plus_left n m : even (n + m) → even n → even m.
Proof.
  intros enm en;
  induction en as [ | n en IHen]; cbn in enm; move enm at bottom;
  [ exact enm | idtac].
  destruct (even_inv enm) as [enm]. exact (IHen enm).
Qed.

Small inversion for smaller inversion: half and its properties

The projection (Braga method)

Definition π even {n} (e: even (S (S n))) : even n :=
  match e in even m return
        let n := match m with S (S n) ⇒ n | _ ⇒ n end in
        let G := match m with S (S n) ⇒ True | _ ⇒ False end in
    G → even n with
  | Ev2 n e ⇒ fun _ ⇒ e
  | _ ⇒ fun fa ⇒ match fa with end
  end I.

Now we can define fixpoints on even n

Fixpoint half n (e: even n) {struct e} : nat :=
  match n return even n → nat with
  | O ⇒ λ _, 0
  | 1 ⇒ λ e , match even_inv e with end
  | S (S n) ⇒ λ e , S (half n (π even e))
  end e.

Partial correctness: half returns the half (no need of inversion because half behaves well)

Lemma double_half : ∀ n e , half n e + half n e = n.
Proof.
  refine (fix fxp n e {struct e} : half n e + half n e = n := _ ).
  destruct e as [ | n e]; cbn.
  - reflexivity.
  - rewrite <- plus_n_Sm. apply f_equal, f_equal, fxp.
Qed.

The result returned byhalf does not depend on the proof argument

Lemma half_pcst : ∀ n (e e' : even n ), half n e = half n e'.
Proof.
  refine (fix fxp n e {struct e} : ∀ e', half n e = half n e' := _ ).
  destruct e as [ | n e]; intro e'; cbn.
  - inversion e' .
    destruct (even_inv e'). reflexivity.
  - destruct (even_inv e') as [e']. cbn. apply f_equal, fxp.
Qed.

even happens to enjoy unicity

Lemma even_unique : ∀n (e e' : even n ), e = e'.
Proof.
  refine (fix fxp n e {struct e} : ∀ e', e = e' := _ ).
  destruct e as [ | n e]; intro e'; cbn.
  - inversion e' .
    Fail dependent inversion e'.
    destruct (even_inv e'). reflexivity.
  - inversion e'; subst . Undo.
    Fail dependent inversion e'.
    destruct (even_inv e') as [e']. apply f_equal, fxp.
Qed.

Fixpoint evenTF n : Prop :=
  match n with
  | O ⇒ True
  | 1 ⇒ False
  | S (S n) ⇒ evenTF n
  end.

Fixpoint even_evenTF {n} (e : even n) : evenTF n :=
  match e in even n return evenTF n with
  | Ev0 ⇒ I
  | Ev2 n e ⇒ even_evenTF e
  end.

Fixpoint evenTF_unique {n} : ∀ (e e' : evenTF n ), e = e'.
Proof.
  refine(match n with O ⇒ _ | 1 ⇒ _ | S (S n) ⇒ _ end);
    cbn; intros e e'.
  - destruct e; destruct e'; reflexivity.
  - destruct e.
  - apply evenTF_unique.
Qed.

Fixpoint evenTF_back n : evenTF n → even n :=
  match n return evenTF n → _ with
  | O ⇒ λ _, Ev0
  | 1 ⇒ λ e , match e with end
  | S (S n) ⇒ λ e , Ev2 n (evenTF_back n e)
  end.
Arguments evenTF_back {n}.

Fixpoint evenTF_mono {n} (e : even n) : e = evenTF_back (even_evenTF e).
Proof.
  destruct e as [ | n e]; cbn.
  - reflexivity.
  - apply f_equal, evenTF_mono.
Qed.

Lemma even_unique_alt {n} (e e' : even n) : e = e'.
Proof.
  rewrite (evenTF_mono e), (evenTF_mono e').
  apply f_equal, evenTF_unique.
Qed.

half_pcst could also be proven as a corollary of even_unique. BUT proof unicity should not be overrated. In other examples such as unbounded linear search, (see ConstructiveEpsilon.v), the result is proof constant WITHOUT unicity of the inductive domain.

Smaller inversion to be used in richer functions such as even_rect

Inductive is_Ev2_π n (e : even (S (S n))) : even (S (S n)) → Prop :=
   | is_Ev2_π _intro : is_Ev2_π n e (Ev2 n (π even e)).

Definition even_inv_π {n} (e : even n) :
    match n return even n → even n → Prop with
    | 0 ⇒ λ _, is_Ev0
    | 1 ⇒ λ _, no_Ev1
    | S (S n) ⇒ is_Ev2_π n
    end e e.
Proof. destruct e; constructor. Defined.

Not that useful in practice (until now)

Definition even_rect
           (P : ∀ n , even n → Type)
           (P0 : P 0 Ev0)
           (P2 : ∀n (e :even n ), P n e → P (S (S n)) (Ev2 n e)) :
  ∀ n (e: even n ), P n e.
Proof.
  refine (
  fix fxp n (e: even n) {struct e} : P n e :=
    match n return ∀ e : even n , P n e with
    | O ⇒ λ e , _
    | 1 ⇒ λ e , match even_inv e with end
    | S (S n) ⇒ λ e , _
    end e).
  - Fail inversion e.
    destruct (even_inv e). apply P0.
  - Fail inversion e.
    destruct (even_inv_π e). apply P2. apply fxp.
Defined.