Library LinAlg.support.finite


Set Implicit Arguments.
Unset Strict Implicit.
Require Export Arith.
Require Export equal_syntax.

  • The setoid of natural numbers - not really necessary but it's nice to have a uniform approach

Definition Nat : Setoid.
apply (Build_Setoid (Equal:=fun i j : nat ⇒ i = j)).
split; try split; red in |- *; unfold app_rel in |- *; simpl in |- *; auto.
intros; transitivity y; auto.
Defined.

  • In this formalisation, we often need the sets We use these for finite sequences: is represented as a setoid function ; also these elements are used as indices into these sequences. Since we use a function type to represent a sequence, we can just type (a i) for .
    • finiteT will serve as the Type on which we base our finite
    setoids (fin N) = .

Record finiteT (N : Nat) : Type := {index : nat; in_range_prf : index < N}.

  • The setoid itself is called (fin N). n:(finiteT N) is really a pair <n,H>; <n,H> and <n',H'> will be deemed equal if n and n' are; the proofs H of n<N and H' of n'(=n)<N may differ.

Definition fin : Nat → Setoid.
intro N.
apply
 (Build_Setoid (Carrier:=finiteT N)
    (Equal:=fun n m : finiteT N ⇒ index n = index m)).
red in |- ×.
split.
red in |- ×.
intro.
red in |- ×.
reflexivity.
red in |- ×.
split.
red in |- ×.
intros.
red in H.
red in H0.
red in |- ×.
transitivity (index y).
assumption.
assumption.
red in |- ×.
intros.
red in H.
red in |- ×.
symmetry in |- ×.
assumption.
Defined.

Lemma fin_equation :
 ∀ (n i j : nat) (Hi : i < n) (Hj : j < n),
 i = j → Build_finiteT Hi =' Build_finiteT Hj in fin n.
intros.
simpl in |- ×.
auto.
Qed.


Hint Resolve fin_equation: algebra.

Lemma fin_decidable :
 ∀ (n : Nat) (i i' : fin n), i =' i' in _ ∨ ¬ i =' i' in _.
intros.
simpl in |- ×.
cut (∀ k l : nat, k = l ∨ k ≠ l).
intro.
auto.
clear i' i n.
double induction k l.
left; auto.
intros; right.
unfold not in |- ×.
intro.
inversion H0.
intros; right.
unfold not in |- ×.
intro.
inversion H0.
intros.
elim (H0 n).
auto.
auto.
Qed.

Lemma fin_O_nonexistent : fin 0 → False.
destruct 1.
inversion_clear in_range_prf0.
Qed.

Hint Resolve fin_O_nonexistent: algebra.

Lemma fin_S_O_unique : ∀ i j : fin 1, i =' j in _.
intro.
case i.
intro x.
case x.
intros l j.
case j.
intro x0.
case x0.
simpl in |- ×.
auto.
intros.
inversion in_range_prf0.
inversion H0.
intros.
inversion in_range_prf0.
inversion H0.
Qed.

Hint Resolve fin_S_O_unique: algebra.

  • A sequence is just a setoid function from (fin n) to A:
Definition seq (n : Nat) (A : Setoid) := MAP (fin n) A.

Lemma toSeq :
 ∀ (A : Setoid) (n : Nat) (v v' : Map (fin n) A),
 v =' v' in seq _ _ → v =' v' in MAP _ _.
auto.
Qed.

Lemma toMap :
 ∀ (A : Setoid) (n : Nat) (v v' : Map (fin n) A),
 v =' v' in MAP _ _ → v =' v' in seq _ _.
auto.
Qed.

Hint Resolve toSeq toMap: algebra.