(*******************************************************************************)
(* Copyright 2018 Catherine Dubois and Alain Giorgetti                         *)
(* Samovar - FEMTO-ST institute                                                *)
(*******************************************************************************)

(*******************************************************************************)
(*      This file is distributed under the terms of the                        *)
(*       GNU Lesser General Public License Version 2.1                         *)
(*******************************************************************************)

(** A [blist] is a list of natural numbers strictly lower than a constant $b$.
 [blist]s represent functions from $\{0,...,n-1\}$ to $\{0,...,b-1\}$ in
 one-line notation. *)

Require Import Arith Arith.Bool_nat Omega List FunInd.
Require Import NPeano.
Require Import listnat.

(** * Characteristic property

 Characterization of lists of natural numbers strictly lower than the constant
 $b$, with an inductive and a Boolean (executable) property. *)

(** ** Inductive property *)

Inductive is_blist (b : nat) : list nat -> Prop :=
| Blist_nil: is_blist b nil
| Blist_cons : forall v l,
   v < b -> is_blist b l
   -> is_blist b (v::l).

(** ** Inductive property with [le]

  The QuickChick feature [Derive] to derive a generator does not work with 
  the inductive predicate [is_blist] because [<] is a notation for [lt] and 
  [lt] is not an inductive property but a definition with [<=] (notation for
  [le]). The following inductive property is equivalent to [is_blist]
  but is defined with the inductive predicate [le] supported by [Derive]. *)

Inductive is_blist_le : nat -> list nat -> Prop :=
| Blist_le_nil : forall b, is_blist_le b nil
| Blist_le_cons : forall v l b,
   v <= b -> is_blist_le (S b) l
   -> is_blist_le (S b) (v :: l).

(** ** Both inductive properties are equivalent *)

Lemma is_blist_eq_def: forall l b, is_blist b l <-> is_blist_le b l.
Proof.
split; induction 1; intros; try constructor.
- {
 case_eq b; intros; subst.
 - omega.
 - constructor. omega. assumption.
}
- omega.
- assumption.
Qed.

(** ** Auxiliary lemmas *)

Lemma is_blist_S : forall b l, is_blist b l -> is_blist (S b) l.
Proof. intros b l H.
induction l.
- apply Blist_nil.
- {
 inversion H; subst.
 apply Blist_cons.
 - omega.
 - apply IHl; assumption.
}
Qed.

Lemma is_blist_le_S : forall b l, is_blist_le b l -> is_blist_le (S b) l.
Proof. intros b l H.
induction l.
- apply Blist_le_nil.
- {
 inversion H; subst.
 apply Blist_le_cons.
 - omega.
 - apply IHl; assumption.
}
Qed.

(** Proved by induction on [l]. *)

(** ** Executable (Boolean) property *)

Fixpoint is_blistb (b : nat) (l : list nat) : bool :=
 match l with
   nil   => true
 | v::l' => (ltb v b) && (is_blistb b l')
 end.

(** ** Consistency between implementation and inductive specifications *)

Lemma is_blist_dec : forall b l, is_blistb b l = true <-> is_blist b l.
Proof. intros b l. split.
- {
 intro H.
 induction l; simpl.
 - apply Blist_nil.
 - {
  simpl in H. apply andb_prop in H. destruct H as [L T].
  apply ltb_lt in L.
  case_eq b; intros; subst.
  - omega.
  - {
   apply Blist_cons.
   - apply L.
   - apply IHl. apply T.
  }
 }
}
- {
 induction 1; simpl; auto.
 apply andb_true_intro. split.
 - apply ltb_lt. assumption.
 - assumption.
}
Qed.

Lemma is_blist_le_dec : forall b l, (is_blistb b l = true <-> is_blist_le b l).
Proof. intros b l. split.
- {
 intro H.
 induction l; simpl.
 - apply Blist_le_nil.
 - {
  simpl in H. apply andb_prop in H. destruct H as [L T]. unfold ltb in L. 
  apply leb_le in L.
  case_eq b; intros; subst.
  - omega.
  - {
   apply Blist_le_cons.
   - omega.
   - apply IHl. apply T.
  }
 }
}
- {
 induction 1; simpl; auto.
 apply andb_true_intro. split.
 - unfold ltb. apply leb_le. omega.
 - assumption.
}
Qed.

(** ** [nil] is a [blist] for any bound [b] *)

Lemma nil_blist : forall b, is_blist b nil.
Proof. intro b. apply is_blist_dec. simpl. auto. Defined.

(** Proved by reflection, with [is_blist_dec]. *)

Lemma nil_blist_le : forall b, is_blist_le b nil.
Proof. intro b. apply is_blist_le_dec. simpl. auto. Defined.

(** Proved by reflection, with [is_blist_le_dec]. *)

(** * Refinement type for [blist]s, based on [is_blist] *)

Record blist (b : nat) : Set := MkBlist {
 blist_val : list nat;
 blist_cstr : is_blist b blist_val
}.

(** ** [blist] constructors based on [is_blist] *)

Definition blist0 (b : nat) : blist b := @MkBlist _ _ (Blist_nil b).

Definition blistS (b v : nat) (pr: v < b) (t : blist b) : blist b :=
 let l := blist_val _ t in
 @MkBlist _ (v :: l) (Blist_cons _ v _ pr (blist_cstr _ t)).

(** * Refinement type for [blist]s, based on [is_blist_le] *)

Record blist_le (b : nat) : Set := MkBlist_le {
 blist_le_val : list nat;
 blist_le_cstr : is_blist_le b blist_le_val
}.

(** ** [blist] constructors based on [is_blist_le] *)

Definition blist_le0 (b : nat) : blist_le b := MkBlist_le _ _ (Blist_le_nil b).

Definition blist_leS (b v : nat) (pr: v <= b) (t : blist_le (S b)) : blist_le (S b) :=
 let l := blist_le_val _ t in
 @MkBlist_le _ (v :: l) (Blist_le_cons _ l _ pr (blist_le_cstr _ t)).

(** * Structure type for [blist]s (based on [is_blist]) *)

(** ** Without size *)

Inductive blistType (b : nat) : Type := 
| B0 : blistType b
| BS : forall i, i < b -> blistType b -> blistType b.

(** ** With size *)

Inductive blistTypeSized (b : nat) : nat -> Type := 
| BS0 : blistTypeSized b 0
| BSS : forall i n, i < b -> blistTypeSized b n -> blistTypeSized b (S n).

(** * Lifting and [blist]s *)

(** *** Some lemmas about Init.Nat.max: *)

(* TODO: find these lemmas in the standard library *)

Lemma max_0 : forall n, max n 0 = n.
Proof.
induction n; simpl; auto.
Qed.

Lemma max_le_l : forall n m, n <= max n m.
Proof.
intros n m.
destruct (le_lt_dec n m).
- rewrite max_r; auto.
- rewrite max_l; omega.
Qed.

Lemma max_le_r : forall n m, n <= max m n.
Proof.
intros n m.
destruct (le_lt_dec n m).
- rewrite max_l; auto.
- rewrite max_r; omega.
Qed.

(* PeanoNat.Nat.le_trans : forall n m p : nat, n <= m -> m <= p -> n <= p *)

(** *** [is_blist] and a larger bound [c]: *)

Lemma is_blist_larger_bound : forall b c l,
 is_blist b l -> b <= c -> is_blist c l.
Proof.
induction 1; intro C.
- apply Blist_nil.
- {
 apply Blist_cons.
 - omega.
 - auto.
}
Qed.

(** *** [is_blist_le] and a larger bound [c]: *)

Lemma is_blist_le_larger_bound : forall b c l,
 is_blist_le b l -> b <= c -> is_blist_le c l.
Proof.
induction 1; intro C.
- apply Blist_le_nil.
- {
 case_eq c; intros; subst.
 - omega.
 - {
  apply Blist_le_cons.
  - omega.
  - auto.
 }
}
Qed.

(** *** [is_blist] and [max]: *)

Lemma is_blist_max : forall b n l,
 is_blist b l -> is_blist (max b n) l.
Proof.
intros. apply is_blist_larger_bound with b; auto.
apply max_le_l.
Qed.

(** *** [is_blist_le] and [max]: *)

Lemma is_blist_le_max : forall b n l,
 is_blist_le b l -> is_blist_le (max b n) l.
Proof.
intros. apply is_blist_le_larger_bound with b; auto.
apply max_le_l.
Qed.

(** ** Lifting, [blist] and max *)

Lemma lift3_blist_max: forall n b (l : list nat) p,
 is_blist b l
 -> is_blist (max b (S n)) (lift3 n p l).
Proof.
intros n b l.
induction l; simpl; intros p H.
- {
 case p; intros; simpl.
 - {
  apply Blist_cons.
  assert (S n <= max b (S n)) as A. apply max_le_r.
  omega.
  apply Blist_nil.
 }
 - {
  apply Blist_cons.
  assert (S n <= max b (S n)) as A. apply max_le_r.
  omega.
  apply Blist_nil.
 }
}
- {
 inversion H; subst.
 case p; intros; simpl.
 - {
  apply Blist_cons.
  - assert (S n <= max b (S n)) as A. apply max_le_r. omega.
  - apply is_blist_max. assumption.
 }
 - {
  apply Blist_cons.
  - assert (b <= max b (S n)) as A. apply max_le_l. omega.
  - apply IHl; auto.
 }
}
Qed.

(** Proved by induction on [l] and then by case on [p], with lemmas about [max]
  and [is_blist]. *)

Lemma lift3_blist_le_max: forall n b (l : list nat) p,
 is_blist_le b l
 -> is_blist_le (max b (S n)) (lift3 n p l).
Proof.
intros n b l p H.
apply is_blist_eq_def.
apply is_blist_eq_def in H.
apply lift3_blist_max. assumption.
Qed.

(** Proved by equivalence between [is_blist_le] and [is_blist] and Lemma [lift3_blist]. *)

(** *** Lifting and blist with max, with [is_blist]: *)

Lemma lift_blist_max: forall b p (l : list nat),
 is_blist b l -> is_blist (max b (S (length l))) (lift p l).
Proof.
unfold lift.
intros b p l.
apply lift3_blist_max.
Qed.

(** *** Lifting and blist with max, with [is_blist_le]: *)

Lemma lift_blist_le_max: forall b p (l : list nat),
 is_blist_le b l -> is_blist_le (max b (S (length l))) (lift p l).
Proof.
unfold lift.
intros b p l.
apply lift3_blist_le_max.
Qed.

(** *** Preservation lemma for lift3, with [is_blist]: *)

Lemma lift3_blist: forall n p (l : list nat) b,
 n < b -> is_blist b l -> is_blist b (lift3 n p l).
Proof.
intros n p l b N B.
assert (max b (S n) = b) as A.
apply max_l. omega.
rewrite <- A.
apply lift3_blist_max. assumption.
Qed.

(** Proved with [lift3_blist_max]. *)

(** *** Preservation lemma for lift3, with [is_blist_le]: *)

Lemma lift3_blist_le: forall n p (l : list nat) b,
 n < b -> is_blist_le b l -> is_blist_le b (lift3 n p l).
Proof.
intros n p l b N B.
assert (max b (S n) = b) as A.
apply max_l. omega.
rewrite <- A.
apply lift3_blist_le_max. assumption.
Qed.

(** Proved with [lift3_blist_le_max]. *)


(** *** Preservation lemma for lift, with [is_blist]: *)

Lemma lift_blist: forall p (l : list nat) b,
 b > length l -> is_blist b l -> is_blist b (lift p l).
Proof.
intros p l b H B.
assert (max b (S (length l)) = b) as A.
apply max_l. omega.
rewrite <- A.
apply lift_blist_max. assumption.
Qed.

(** Proved with [lift_blist_max]. *)

(** *** Preservation lemma for lift, with [is_blist_le]: *)

Lemma lift_blist_le: forall p (l : list nat) b,
 b > length l -> is_blist_le b l -> is_blist_le b (lift p l).
Proof.
intros p l b H B.
assert (max b (S (length l)) = b) as A.
apply max_l. omega.
rewrite <- A.
apply lift_blist_le_max. assumption.
Qed.

(** Proved with [lift_blist_le_max]. *)

(** * Bounded list and reversing function. *)

(** ** Auxiliary lemma *)
Lemma is_blist_snoc : forall v l b, v < b -> is_blist b l
 -> is_blist b (l ++ v :: nil).
Proof.
intros v l b V.
induction 1; simpl.
- apply Blist_cons. auto. constructor.
- apply Blist_cons. auto. apply IHis_blist.
Qed.

Lemma rev_blist: forall ( l : list nat) (b : nat), is_blist b l -> is_blist b (rev l).
Proof.
induction 1; simpl; try constructor.
apply is_blist_snoc; auto.
Qed.
