E1: Wektory, czyli listy indeksowane długością [TODO]


(*Require Import Coq.Classes.Morphisms.
Require Export MyList.
Require Import Monads.
Require Import JMeq.
Require Import Ring.*)

Require Import List.
Import ListNotations.

Require Import JMeq.
Require Import Eqdep.
Require Import Arith.

Arguments eq_dep [U P p] _ [q] _.

Set Implicit Arguments.

Inductive vec (A : Type) : nat -> Type :=
| vnil : vec A 0
| vcons : forall n : nat, A -> vec A n -> vec A (S n).

Arguments vnil {A}.
Arguments vcons {A n} _ _.

Podstawowe funkcje

length

Zdefiniuj funkcję len, która oblicza długość listy. Powinna ona wykonywać się w czasie liniowym.


Lemma len_vnil :
  forall A : Type, len (@vnil A) = 0.

Lemma len_vcons' :
  forall (A : Type) (n : nat) (h : A) (t : vec A n),
    len (vcons h t) = S n.

Lemma len_vcons :
  forall (A : Type) (n : nat) (h : A) (t : vec A n),
    len (vcons h t) = S (len t).

app

Zdefiniuj funkcję app, która skleja dwie listy.


Notation "l1 +++ l2" := (app l1 l2) (at level 40).

Lemma app_vnil_l :
  forall (A : Type) (n : nat) (l : vec A n), vnil +++ l = l.

Lemma JMeq_vcons :
  forall (A : Type) (n m : nat) (h h' : A) (t : vec A n) (t' : vec A m),
    n = m -> JMeq h h' -> JMeq t t' -> JMeq (vcons h t) (vcons h' t').
(* end hide *)
Proof.
  intros. subst. reflexivity.
Qed.
(* end hide *)

Lemma app_vnil_r :
  forall (A : Type) (n : nat) (l : vec A n), JMeq (l +++ vnil) l.

Lemma app_vnil_r' :
  forall (A : Type) (n : nat) (l : vec A n), eq_dep (l +++ vnil) l.

Lemma app_assoc :
  forall (A : Type) (x y z : nat) (l1 : vec A x) (l2 : vec A y) (l3 : vec A z),
    eq_dep (l1 +++ (l2 +++ l3)) ((l1 +++ l2) +++ l3).

Lemma app_assoc' :
  forall (A : Type) (x y z : nat) (l1 : vec A x) (l2 : vec A y) (l3 : vec A z),
    JMeq (l1 +++ (l2 +++ l3)) ((l1 +++ l2) +++ l3).

Lemma app_len :
  forall (A : Type) (n m : nat) (l1 : vec A n) (l2 : vec A m),
    len (l1 +++ l2) = len l1 + len l2.

Lemma app_cons :
  forall (A : Type) (n m : nat) (x : A) (l1 : vec A n) (l2 : vec A m),
    (vcons x l1) +++ l2 = vcons x (l1 +++ l2).

Lemma app_cons2 :
  forall (A : Type) (n m : nat) (x : A) (l1 : vec A n) (l2 : vec A m),
    JMeq (l1 +++ vcons x l2) ((l1 +++ (vcons x vnil)) +++ l2).

Lemma app_cons2' :
  forall (A : Type) (n m : nat) (x : A) (l1 : vec A n) (l2 : vec A m),
    eq_dep (l1 +++ vcons x l2) ((l1 +++ (vcons x vnil)) +++ l2).

Require Import Lia Arith.

Lemma no_infinite_cons :
  forall (A : Type) (n : nat) (h : A) (t : vec A n),
    eq_dep t (vcons h t) -> False.

Lemma no_infinite_app :
  forall (A : Type) (n m : nat) (l : vec A n) (l' : vec A m),
    ~ eq_dep l' vnil -> eq_dep l (l' +++ l) -> False.

Lemma app_inv1 :
  forall (A : Type) (n m : nat) (l : vec A n) (l1 l2 : vec A m),
    l +++ l1 = l +++ l2 -> l1 = l2.

Lemma is_vnil :
  forall (A : Type) (n : nat) (l : vec A n),
    {eq_dep l vnil} + {~ eq_dep l vnil}.

Require Import Coq.Program.Equality.

Lemma app_inv2 :
  forall (A : Type) (n m : nat) (l : vec A n) (l1 l2 : vec A m),
    eq_dep (l1 +++ l) (l2 +++ l) -> eq_dep l1 l2.

Lemma app_eq_nil :
  forall (A : Type) (n m : nat) (l1 : vec A n) (l2 : vec A m),
    eq_dep (l1 +++ l2) vnil -> eq_dep l1 vnil /\ eq_dep l2 vnil.

Zdefiniuj funkcję rev, która odwraca listę. Wskazówka: definicja podobna do tej dla list nie zadziała. Napiszę wcześniej funkcję pomocniczą snoc, która wstawia element na koniec wektora.


Notation "[ ]" := vnil.
Notation "h :: t" := (vcons h t).
Notation "l1 ++ l2" := (app l1 l2).

Lemma rev_nil :
  forall (A : Type), rev [] = @vnil A.

Lemma rev_length :
  forall (A : Type) (n : nat) (l : vec A n),
    len (rev l) = len l.

Lemma snoc_app :
  forall (A : Type) (x : A) (n m : nat) (l1 : vec A n) (l2 : vec A m),
    eq_dep (snoc x (l1 +++ l2)) (l1 +++ snoc x l2).

Lemma rev_app :
  forall (A : Type) (n m : nat) (l1 : vec A n) (l2 : vec A m),
    eq_dep (rev (l1 +++ l2)) (rev l2 +++ rev l1).

Lemma snoc_rev :
  forall (A : Type) (n : nat) (x : A) (l : vec A n),
    rev (snoc x l) = vcons x (rev l).

Lemma rev_rev :
  forall (A : Type) (n : nat) (l : vec A n), rev (rev l) = l.

Zdefiniuj induktywny predykat elem. elem x l jest spełniony, gdy x jest elementem wektora l.


Lemma elem_nil :
  forall (A : Type) (x : A), ~ elem x vnil.

Lemma elem_inv_head :
  forall (A : Type) (n : nat) (x h : A) (t : vec A n),
    ~ elem x (vcons h t) -> x <> h.

Lemma elem_inv_tail :
  forall (A : Type) (n : nat) (x h : A) (t : vec A n),
    ~ elem x (h :: t) -> ~ elem x t.

Lemma elem_app_l :
  forall (A : Type) (n m : nat) (x : A) (l1 : vec A n) (l2 : vec A m),
    elem x l1 -> elem x (l1 ++ l2).

Lemma elem_app_r :
  forall (A : Type) (n m : nat) (x : A) (l1 : vec A n) (l2 : vec A m),
    elem x l2 -> elem x (l1 ++ l2).

Lemma elem_app_or :
  forall (A : Type) (n m : nat) (x : A) (l1 : vec A n) (l2 : vec A m),
    elem x (l1 ++ l2) -> elem x l1 \/ elem x l2.

Lemma elem_or_app :
  forall (A : Type) (n m : nat) (x : A) (l1 : vec A n) (l2 : vec A m),
    elem x l1 \/ elem x l2 -> elem x (l1 ++ l2).

Lemma elem_snoc :
  forall (A : Type) (n : nat) (x : A) (l : vec A n),
    elem x (snoc x l).

Lemma elem_snoc' :
  forall (A : Type) (n : nat) (x y : A) (l : vec A n),
    elem x l -> elem x (snoc y l).

Lemma elem_snoc'' :
  forall (A : Type) (n : nat) (x y : A) (l : vec A n),
    elem x (snoc y l) <-> x = y \/ elem x l.

Lemma elem_rev :
  forall (A : Type) (n : nat) (x : A) (l : vec A n),
    elem x l -> elem x (rev l).

Lemma elem_rev_conv :
  forall (A : Type) (n : nat) (x : A) (l : vec A n),
    elem x (rev l) -> elem x l.

Lemma elem_split :
  forall (A : Type) (n : nat) (x : A) (l : vec A n),
    elem x l -> exists (m1 m2 : nat) (l1 : vec A m1) (l2 : vec A m2),
      eq_dep l (l1 ++ x :: l2).

Zdefiniuj funkcję map, która aplikuje funkcję f do każdego elementu listy.


Lemma map_id : forall (A : Type) (n : nat) (l : vec A n),
  map id l = l.

Lemma map_comp :
  forall (A B C : Type) (n : nat) (f : A -> B) (g : B -> C)
    (l : vec A n), map g (map f l) = map (fun x : A => g (f x)) l.

Lemma map_length :
  forall (A B : Type) (n : nat) (f : A -> B) (l : vec A n),
    len (map f l) = len l.

Lemma map_app :
  forall (A B : Type) (n m : nat) (f : A -> B) (l1 : vec A n) (l2 : vec A m),
    map f (l1 ++ l2) = map f l1 ++ map f l2.

Lemma elem_map :
  forall (A B : Type) (n : nat) (f : A -> B) (l : vec A n) (x : A),
    elem x l -> elem (f x) (map f l).

Lemma elem_map_conv :
  forall (A B : Type) (n : nat) (f : A -> B) (l : vec A n) (y : B),
    elem y (map f l) <-> exists x : A, f x = y /\ elem x l.

Lemma map_snoc :
  forall (A B : Type) (n : nat) (f : A -> B) (x : A) (l : vec A n),
    map f (snoc x l) = snoc (f x) (map f l).

Lemma map_rev :
  forall (A B : Type) (n : nat) (f : A -> B) (l : vec A n),
    map f (rev l) = rev (map f l).

Lemma map_ext_elem :
  forall (A B : Type) (n : nat) (f g : A -> B) (l : vec A n),
    (forall x : A, elem x l -> f x = g x) -> map f l = map g l.

Lemma map_ext :
  forall (A B : Type) (n : nat) (f g : A -> B) (l : vec A n),
    (forall x : A, f x = g x) -> map f l = map g l.

Napisz funkcję join, która spłaszcza listę list.


Lemma join_app :
  forall (A : Type) (n n' m m' : nat) (l1 : vec (vec A n) m)
  (l2 : vec (vec A n) m'),
    eq_dep (join (l1 ++ l2)) (join l1 ++ join l2).

Lemma join_map :
  forall (A B : Type) (n m : nat) (f : A -> B) (l : vec (vec A n) m),
    map f (join l) = join (map (map f) l).

repeat

Zdefiniuj funkcję repeat, która zwraca listę n powtórzeń wartości x.


Lemma repeat_len :
  forall (A : Type) (n : nat) (x : A),
    len (repeat n x) = n.

Lemma repeat_elem :
  forall (A : Type) (n : nat) (x y : A),
    elem x (repeat n y) -> x = y.

nth

Zdefiniuj funkcję nth, która zwraca n-ty element listy lub None, gdy nie ma n-tego elementu.


Lemma nth_len :
  forall (A : Type) (m n : nat) (l : vec A n),
    m < n -> exists x : A, nth m l = Some x.

Require Import Arith.

Lemma nth_elem :
  forall (A : Type) (m n : nat) (l : vec A n),
    m < n -> exists x : A, nth m l = Some x /\ elem x l.

Lemma nth_elem_conv :
  forall (A : Type) (n : nat) (x : A) (l : vec A n),
    elem x l -> exists m : nat, nth m l = Some x.

Lemma nth_overflow :
  forall (A : Type) (m n : nat) (l : vec A n),
    n <= m -> ~ exists x : A, nth m l = Some x.

Lemma nth_app1 :
  forall (A : Type) (m n1 n2 : nat) (l1 : vec A n1) (l2 : vec A n2),
    m < n1 -> nth m (l1 ++ l2) = nth m l1.

Lemma nth_app2 :
  forall (A : Type) (m n1 n2 : nat) (l1 : vec A n1) (l2 : vec A n2),
    n1 <= m -> nth m (l1 ++ l2) = nth (m - n1) l2.

Lemma nth_split :
  forall (A : Type) (m n : nat) (l : vec A n) (x : A),
    nth m l = Some x -> exists (n1 n2 : nat) (l1 : vec A n1) (l2 : vec A n2),
      eq_dep l (l1 ++ x :: l2) /\ n1 = m.

Lemma nth_None :
  forall (A : Type) (m n : nat) (l : vec A n),
    nth m l = None -> n <= m.

Lemma nth_Some :
  forall (A : Type) (m n : nat) (l : vec A n) (x : A),
    nth m l = Some x -> m < n.

Lemma map_nth :
    forall (A B : Type) (m n : nat) (f : A -> B) (l : vec A n) (x : A),
      nth m l = Some x -> nth m (map f l) = Some (f x).

head i last

Zdefiniuj funkcje head i last, które zwracają odpowiednio pierwszy i ostatni element listy (lub None, jeżeli jest pusta).


Lemma head_cons :
  forall (A : Type) (n : nat) (h : A) (t : vec A n),
    head (h :: t) = h.

Lemma last_snoc :
  forall (A : Type) (n : nat) (h : A) (t : vec A n),
    last (snoc h t) = h.

Lemma head_nth:
  forall (A : Type) (n : nat) (l : vec A (S n)),
    Some (head l) = nth 0 l.

Lemma last_nth : forall (A : Type) (n : nat) (l : vec A (S n)),
  Some (last l) = nth n l.

tail i init

Zdefiniuj funkcje tail i init, które zwracają odpowiednio ogon listy oraz wszystko poza jej ostatnim elementem. Użyj typów zależnych.


take i drop

Zdefiniuj funkcje take i drop, które odpowiednio biorą lub odrzucają n pierwszych elementów listy.


Lemma take_nil :
  forall (A : Type) (n : nat),
    eq_dep (take n []) (@vnil A).

Lemma drop_nil :
  forall (A : Type) (n : nat),
    eq_dep (drop n []) (@vnil A).

Lemma take_cons :
  forall (A : Type) (n m : nat) (h : A) (t : vec A n),
    take (S m) (h :: t) = h :: take m t.

Lemma drop_cons :
  forall (A : Type) (n m : nat) (h : A) (t : vec A n),
    drop (S m) (h :: t) = drop m t.

Lemma take_0 :
  forall (A : Type) (n : nat) (l : vec A n),
    take 0 l = [].

Lemma drop_0 :
  forall (A : Type) (n : nat) (l : vec A n),
    eq_dep (drop 0 l) l.

Lemma take_length :
  forall (A : Type) (n : nat) (l : vec A n),
    eq_dep (take n l) l.

Lemma drop_all :
  forall (A : Type) (n : nat) (l : vec A n),
    eq_dep (drop n l) [].

Lemma take_length' :
  forall (A : Type) (n m : nat) (l : vec A n),
    n <= m -> eq_dep (take m l) l.

Lemma drop_length' :
  forall (A : Type) (m n : nat) (l : vec A n),
    n <= m -> eq_dep (drop m l) [].

Lemma length_take :
  forall (A : Type) (m n : nat) (l : vec A n),
    len (take m l) = min m n.

Lemma drop_take :
  forall (A : Type) (m n : nat) (l : vec A n),
    m <= n -> len (drop m l) = n - m.

Lemma take_map :
  forall (A B : Type) (f : A -> B) (m n : nat) (l : vec A n),
    map f (take m l) = take m (map f l).

Lemma drop_map :
  forall (A B : Type) (f : A -> B) (m n : nat) (l : vec A n),
    eq_dep (map f (drop m l)) (drop m (map f l)).

Lemma take_elem :
  forall (A : Type) (m n : nat) (l : vec A n) (x : A),
    elem x (take m l) -> elem x l.

Lemma drop_elem :
  forall (A : Type) (m n : nat) (l : vec A n) (x : A),
    elem x (drop m l) -> elem x l.

Lemma take_take :
  forall (A : Type) (m m' n : nat) (l : vec A n),
    eq_dep (take m (take m' l)) (take m' (take m l)).

Lemma drop_S :
  forall (A : Type) (m m' n : nat) (l : vec A n),
    eq_dep (drop (S m) (drop m' l)) (drop m (drop (S m') l)).

Lemma drop_drop :
  forall (A : Type) (m m' n : nat) (l : vec A n),
    eq_dep (drop m (drop m' l)) (drop m' (drop m l)).



Lemma take_drop :
  forall (A : Type) (a b n : nat) (l : vec A n),
    eq_dep (take a (drop b l)) (drop b (take (b + a) l)).

Predykaty i relacje (TODO)

Tutaj coś jak bycie elementem albo podwektorem.