Library BoundedNat.bounded_even

Author: Jean-François Monin, Verimag, Université Grenoble Alpes
Even bounded natural numbers and half
  • computing the half using the Braga method without graph
  • definition of even_rect using even_inv_π = combination small inversion + projection ⟶ the technique works on "second level dependent types" as well

Require Import Utf8 bounded_nat looping_absurd.

Definition of even

Inductive even : ∀ {n}, t n → Prop :=
  | even_0 {n} : even (@FO n)
  | even_2 {n} (i: t n) : even i → even (FS (FS i)).

Small inversion
Inductive is_even_0 {n} : even (@FO n) → Prop :=
   | is_even_0_intro : is_even_0 even_0.

Inductive no_even1 {n} : even (FS (@FO n)) → Prop :=.

Inductive is_even_2 {n} (i: t n) : even (FS (FS i)) → Prop :=
   | is_even_2_intro (e : even i) : is_even_2 i (even_2 i e).

Definition even_inv {n} {i : t n} (e : even i) :
    match i return even i → Prop with
    | @FO n ⇒ is_even_0
    | FS i ⇒
        match i return even (FS i) → Prop with
        | @FO n ⇒ no_even1
        | FS i ⇒ is_even_2 i
        end
    end e.
Proof. destruct e; constructor. Defined.

Simple Applications

The basic one
Lemma even_2_inv : ∀ n (i: t n), even (FS (FS i)) → even i.
Proof.
  intros n i e.
  inversion e. subst.
terrific
Undo 2.
  destruct (even_inv e) as [e]. exact e.
Qed.

Additions and even numbers.
We show even (i + j) → even i → even j on bounded natural numbers.

Fixpoint even_lift1 m {n} {i: t n} : even (lift1 m i) → even i.
Proof.
  intro e.
  destruct i as [ | n i]; simpl in e.
  - constructor 1.
  - destruct i as [ | n i];
      repeat (unfold t_n_Sm in e; rewrite <- plus_n_Sm in e; simpl in e).
    + destruct (even_inv e).
    + destruct (even_inv e) as [e]. constructor 2. apply (even_lift1 m n i e).
Qed.

Lemma even_plus_left n m (i: t n) (j: t m) : even (Fplus i j) → even i → even j.
Proof.
  intros eij ei.
  induction ei as [ | n i ei IHei]; simpl in eij.
  - apply (even_lift1 (S n) eij).
  - inversion eij. subst.
terrific !
Undo 2.
    destruct (even_inv eij) as [eij]. exact (IHei eij).
Qed.

Remark: another lifting function can be defined as well.
Simpler than lift1, but unused here
Fixpoint lift2 {n} (i : t n) m : t (n + m) :=
  match i in t n return t (n + m) with
  | FO ⇒ FO
  | FS i ⇒ FS (lift2 i m)
  end.

Fixpoint even_lift2 {n} (i: t n) : ∀ m, even (lift2 i m) → even i.
Proof.
  intros m e.
  destruct i as [ | n i]; simpl in e.
  - constructor 1.
  - destruct i as [ | n i]; simpl in e.
    + destruct (even_inv e).
    + destruct (even_inv e) as [e]. constructor 2. apply (even_lift2 n i m e).
Qed.

Computation of the half of an even bounded natural number i.

The termination certificate for input i is the proof of even i
Defining the desired projection even (FS (FS i)) → even i requires auxiliary administrative steps relating the double predecessor of i : t n with the double predecessor of n. Unfortunately, the predecessor functions need to be guarded (no default value is available at call), hence the use of Fexc from looping_absurd.
GUARDS
Definition is_S_S n : Prop :=
  match n with S (S n) ⇒ T | _ ⇒ F end.

Definition is_FS_FS {n} (i: t n) : Prop :=
  match i with FS (FS i) ⇒ T | _ ⇒ F end.

Guard conversion
Interactive version
Lemma iFF_iSS_inter {n} (i : t n): is_FS_FS i → is_S_S n.
Proof.
  destruct i as [ | n1 [ | n2 i]]; intro G; now case G.
Qed.

Explicit version
Definition iFF_iSS {n} {i: t n} : is_FS_FS i → is_S_S n :=
  match i in t n return is_FS_FS i → is_S_S n with
 | FO ⇒ fun fa ⇒ match fa with end
 | FS i ⇒
     match i in t n return is_FS_FS (FS i) → is_S_S (S n) with
     | FO ⇒ fun fa ⇒ match fa with end
     | FS i ⇒ fun _ ⇒ I
     end
 end.

Guarded double predecessors
Definition pr2 n : is_S_S n → nat :=
  match n with
  | S (S x) ⇒ fun _ ⇒ x
  | _ ⇒ fun fa ⇒ Fexc fa
  end.

Definition fpred2 {m} (j: t m) : ∀ G : is_FS_FS j, t (pr2 m (iFF_iSS G)) :=
  match j in t m return ∀ G: is_FS_FS j, t (pr2 m (iFF_iSS G)) with
  | FS j ⇒
    match j in t m return ∀ G: is_FS_FS (FS j), t (pr2 (S m) (iFF_iSS G)) with
    | FS j ⇒ fun _ ⇒ j
    | _ ⇒ fun fa ⇒ Fexc fa
    end
  | _ ⇒ fun fa ⇒ Fexc fa
  end.

The projection
Definition πeven {n} {i: t n} (D: even (FS (FS i))) : even i :=
  match D in even j return
    ∀ G: is_FS_FS j, even (fpred2 j G) with
  | even_2 i e ⇒ fun _ ⇒ e
  | _ ⇒ fun fa ⇒ match fa with end
  end I.

Smaller inversion to be used for defining richer functions such as even_rect
Inductive is_even_2_π {n} (i: t n) (e : even (FS (FS i))) : even (FS (FS i)) → Prop :=
   | is_even_2_π_intro : is_even_2_π i e (even_2 i (πeven e)).

Definition even_inv_π {n} {i : t n} (e : even i) :
  match i return even i → even i → Prop with
    | @FO n ⇒ fun _ ⇒ is_even_0
    | FS i ⇒
        match i return even (FS i) → even (FS i) → Prop with
        | @FO n ⇒ fun _ ⇒ no_even1
        | FS i ⇒ fun e ⇒ is_even_2_π i e
        end
    end e e.
Proof. destruct e; constructor. Defined.

Now we can define fixpoints on even i
Fixpoint half_in_nat {n} (i: t n) (D: even i) {struct D} : nat :=
  match i with
  | FO ⇒ fun _ ⇒ 0
  | FS i ⇒
    match i return even (FS i) → nat with
    | FO ⇒ fun D ⇒ (Fexc (match even_inv D with end))
    | FS i ⇒ fun D ⇒ S (half_in_nat i (πeven D))
    end
  end D.

A proof by fixpoint
Fixpoint double_half_in_nat {n} (i: t n) (D: even i) {struct D} :
  let h := half_in_nat i D in forget i = h + h.
Proof.
  destruct D as [n | n i D]; cbn.
  - reflexivity.
  - rewrite (double_half_in_nat n i D).
    set (h := half_in_nat i D). rewrite plus_n_Sm. reflexivity.
Qed.

General recursion principle on bounded even numbers
Crucial use of even_inv_π
Definition even_rect (P : ∀ n (i : t n), even i → Type)
         (P0 : ∀n, P (S n) (@FO n) even_0)
         (P2 : ∀n (i : t n) (e :even i), P n i e → P (S (S n)) (FS (FS i)) (even_2 i e)) :
  ∀ {n} (i: t n) (e: even i), P n i e.
Proof.
  refine (
  fix fxp {n} (i: t n) (e: even i) {struct e} : P n i e :=
    match i in t n return ∀ e : even i, P n i e with
    | FO ⇒ fun e ⇒ _
    | FS i ⇒
        match i in t n return ∀ e : even (FS i), P (S n) (FS i) e with
        | FO ⇒ fun e ⇒ (Fexc (match even_inv e with end))
        | FS i ⇒ fun e ⇒ _
        end
    end e).
  - destruct (even_inv e). apply P0.
  - destruct (even_inv_π e). apply P2. apply fxp.
Defined.

For programming purposes
Definition even_fold := even_rect.
Arguments even_fold {P} P0 P2 {n}.

Previous exercise using this induction principle

Lemma double_half_in_nat_by_rect {n} (i: t n) (D: even i) :
  let h := half_in_nat i D in forget i = h + h.
Proof.
  induction D as [n | n i D HD] using even_rect; cbn.
  - reflexivity.
  - rewrite HD.
    set (h := half_in_nat i D). rewrite plus_n_Sm. reflexivity.
Defined.

A less coarse half function
Fixpoint half_in_t {n} (i: t n) (D: even i) {struct D} : t n :=
  match i in t n return even i → t n with
  | FO ⇒ fun _ ⇒ FO
  | FS i ⇒
    match i in t n return even (FS i) → t (S n) with
    | FO ⇒ fun D ⇒ (Fexc (match even_inv D with end))
    | FS i ⇒ fun D ⇒ FS (lift1 1 (half_in_t i (πeven D)))
    end
  end D.

Definition half_in_t_by_fold {n} (i: t n) (e: even i) : t n :=
  even_fold
     (fun n ⇒ @FO n)
     (fun n i e ha ⇒ FS (lift1 1 ha)) i e.