smaller inversions

bounded_nat.v

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

(** ------------------------------------------------------------ *)
(** Similar to finite_set from itp13 with
- [odd/F1] renamed as [even/FO]
- the parameter is the cardinal
- definition of addition (to be used in even_bounded_nat)
*)

Require Import Utf8.
From Coq Require Import ssreflect ssrbool ssrfun.
From mathcomp Require Import ssrnat.


(*=============================================================== *)
(** Bounded natural numbers *)

(** The type [t n] represents a finite set of cardinal [n],
   whose elements are numbered from FO to FS (... (FS FO)   *)
Inductive t : nat → Set :=
  | FO {n} : t n.+1
  | FS {n} : t n → t n.+1.

Fixpoint forget {n} (i : t n) : nat :=
  match i with
  | FO _ => O
  | FS _ i => (forget i).+1
  end.

(** Small inversion. *)

(** Here we have no shape for 0 and 2 shapes for [(S n)] *)
Inductive shape_O : t 0 → Set :=.

Inductive shape_S (n : nat) : t (S n) → Set :=
  | shape_S_F0 : shape_S n FO
  | shape_S_FS : ∀ i : t n, shape_S n (FS i).

Definition t_inv {n} (i : t n) :
    match n with
    | O => shape_O
    | S n => shape_S n
    end i.
Proof. by case: i=>{}n; constructor. Defined.

(** Generic use *)
Section sec_example.
  Variable P : forall n, t n → Prop.
  Lemma case_t_S n :
    P n.+1 FO → (forall i, P n.+1 (FS i)) →
    forall (i : t n.+1), P n.+1 i.
  Proof.
  move=>P0 PS i.
  case: (t_inv i)=>[|{}i].
  - by exact: P0.
  by apply: PS.
  Qed.
End sec_example.

(** Addition *)
(**
   An administrative lifting function ([lift1]) is needed.
 *)

Definition t_n_Sm {n m} (i: t (S (m + n))) : t (m + S n).
by rewrite addnS.
Defined.

Fixpoint lift1 m {n} (i : t n) : t (m + n) :=
  match i in t n return t (m + n) with
  | FO _ => t_n_Sm FO
  | FS _ i => t_n_Sm (FS (lift1 m i))
  end.

Fixpoint Fplus {n m : nat} (i : t n) (j : t m) : t (n + m) :=
  match i with
  | FO n => lift1 n.+1 j
  | FS _ i => FS (Fplus i j)
  end.

even_half.v

(** 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.
From Coq Require Import ssreflect ssrbool ssrfun.
From mathcomp Require Import ssrnat.

(** ------------------------------------------------------------ *)
(** * Definition of [even] and its small inversion *)
Inductive even : forall n, Prop :=
  | even_0 :            even 0
  | even_2 n : even n → even n.+2.

(** Small inversion *)
Inductive is_even_0 : even 0 → Prop :=
   | is_even_0_intro : is_even_0 even_0.
Inductive no_even1 : even 1 → Prop :=.
Inductive is_even_2 n : even n.+2 → Prop :=
   | is_even_2_intro (e : even n) : is_even_2 n (even_2 n e).

Definition even_inv {n} (e : even n) :
    match n return even n → Prop with
    | 0 => is_even_0
    | 1 => no_even1
    | n.+2 => is_even_2 n
    end e.
Proof. by case: e. Defined.

Print even_inv.

(* Basic usage of small inversion *)
Lemma even_plus_left n m : even (n + m) → even n → even m.
Proof.
move=>enm en; elim: _ / en enm => //{}n en IHen.
by rewrite !addSn => enm; case: (even_inv enm).
Qed.

(** ------------------------------------------------------------------- *)
(** * Small inversion for smaller inversion: [half] and its properties *)

(** The projection (Braga method) *)
Definition πeven {n} (e: even n.+2) : even n :=
  match e in even m return
        let n := match m with n.+2 => n | _ => n end in
        let G := match m with _.+2 => True | _ => False end in
    G -> even n with
  | even_2 n e => fun G => e
  | _ => fun G => match G with end
  end I.

(** Now we can define fixpoints on [even n] *)
Fixpoint hlf n (e: even n) {struct e} : nat :=
  match n return even n -> nat with
  | O => λ _, 0
  | 1 => λ e, match even_inv e with end
  | n.+2 => λ e, (hlf n (πeven e)).+1
  end e.

(** Partial correctness: [half] returns the half
    (no need of inversion because [half] behaves well) *)
Lemma double_half : ∀ n e, hlf n e + hlf n e = n.
Proof.
refine (fix fxp n e {struct e} : hlf n e + hlf n e = n := _ ).
case: _ / e => /= [|{}n e] //.
by rewrite addSn addnS; congr _.+2; exact: fxp.
Qed.

(** [half] is proof irrelevant *)
Lemma half_pirr : ∀ n (e e' : even n), hlf n e = hlf n e'.
Proof.
refine (fix fxp n e {struct e} : ∀ e', hlf n e = hlf n e' := _ ).
case: _ / e => /= [|{}n e] e'; case: (even_inv e')=>//= {}e'.
by congr _.+1; exact: 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' := _ ).
case: _ / e => /= [|{}n e] e'; case: (even_inv e'); first by reflexivity.
by move=>{}e'; congr (even_2 n); exact: fxp.
Qed.

(** [half_pirr] 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 irrelevant
    WITHOUT unicity of the inductive domain. *)

(** ------------------------------------------------------------------ *)
(** * Smaller inversion to be used in richer functions such as even_rect *)
Inductive is_even_2_π n (e : even n.+2) : even n.+2 → Prop :=
   | is_even_2_π_intro : is_even_2_π n e (even_2 n (πeven e)).

Definition even_inv_π {n} (e : even n) :
    match n return even n → even n → Prop with
    | 0 => λ _, is_even_0
    | 1 => λ _, no_even1
    | n.+2 => is_even_2_π n
    end e e.
Proof. by case: e. Defined.


(** Not that useful in practice (until now) *)
Definition even_rect
           (P : ∀ n, even n -> Type)
           (P0 : P 0 even_0)
           (P2 : ∀n (e :even n), P n e → P (S (S n)) (even_2 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
    | n.+2 => λ e, _
    end e).
- by case: (even_inv e); exact: P0.
by case: (even_inv_π e); apply: P2; exact: fxp.
Defined.