lesson2_part1.v

Authors:

Yannick Forster

Théo Winterhalter

Files:

Display all goals and responses

Lists

The type of list is both recursive and has a type parameter.

Inductive list (A : Type) :=
| nil : list A
| cons : A -> list A -> list A.

We declare arguments as implicit. Note here we can specify a prefix if we want.

Arguments nil {A}.
Arguments cons {A}.

Set Printing Implicit.
Compute (cons 5 nil).= @cons nat 5 (@nil nat)
: list nat
Unset Printing Implicit.

Check now the induction principle we get for lists. It's saying that to prove P l for some list l, you only need to prove

P nil

P (cons a l') for any a and l' such that P l'

Have a look at its type:

Check list_ind.list_ind
     : forall (A : Type) (P : list A -> Prop),
       P nil ->
       (forall (a : A) (l : list A), P l -> P (cons a l)) ->
       forall l : list A, P l

Proofs by induction

We reimport all these datatypes from Rocq, to be able to use functions from the standard library.

From Stdlib  Require Import Datatypes List.
Open Scope nat.

Like for nat, list in the standard library comes with nice notations to be able to write x :: l or [ a ; b ; c ; d ]. We can load them as follows.

Import ListNotations.

Below we check the types of concatenation and reversal of lists.

About app.app : forall [A : Type], list A -> list A -> list A

app is not universe polymorphic
Arguments app [A]%_type_scope (_ _)%_list_scope
app is transparent
Expands to: Constant Corelib.Init.Datatypes.app
Declared in library Corelib.Init.Datatypes, line 355, characters 11-14
About rev.rev : forall [A : Type], list A -> list A

rev is not universe polymorphic
Arguments rev [A]%_type_scope l%_list_scope
rev is transparent
Expands to: Constant Stdlib.Lists.List.rev
Declared in library Stdlib.Lists.List, line 978, characters 11-14

Lemmas about lists we typically proven by induction as we did for natural numbers.

Lemma app_nil_r A (l : list A) :
  l ++ nil = l.A: Type
l: list A
l ++ [] = l
Proof.A: Type
l: list A
l ++ [] = l
  induction l.A: Type
[] ++ [] = []
A: Type
a: A
l: list A
IHl: l ++ [] = l
(a :: l) ++ [] = a :: l all: simpl.A: Type
[] = []
A: Type
a: A
l: list A
IHl: l ++ [] = l
a :: l ++ [] = a :: l
  -A: Type
[] = [] reflexivity.
  -A: Type
a: A
l: list A
IHl: l ++ [] = l
a :: l ++ [] = a :: l f_equal.A: Type
a: A
l: list A
IHl: l ++ [] = l
l ++ [] = l assumption.
Qed.

Lemma rev_app_distr {A} (l1 l2 : list A) :
  rev (l1 ++ l2) = rev l2 ++ rev l1.A: Type
l1, l2: list A
rev (l1 ++ l2) = rev l2 ++ rev l1
Proof.A: Type
l1, l2: list A
rev (l1 ++ l2) = rev l2 ++ rev l1
  induction l1 as [| a l IHl].A: Type
l2: list A
rev ([] ++ l2) = rev l2 ++ rev []
A: Type
a: A
l, l2: list A
IHl: rev (l ++ l2) = rev l2 ++ rev l
rev ((a :: l) ++ l2) = rev l2 ++ rev (a :: l) all: simpl.A: Type
l2: list A
rev l2 = rev l2 ++ []
A: Type
a: A
l, l2: list A
IHl: rev (l ++ l2) = rev l2 ++ rev l
rev (l ++ l2) ++ [a] = rev l2 ++ rev l ++ [a]
  -A: Type
l2: list A
rev l2 = rev l2 ++ [] rewrite app_nil_r.A: Type
l2: list A
rev l2 = rev l2 reflexivity.
  -A: Type
a: A
l, l2: list A
IHl: rev (l ++ l2) = rev l2 ++ rev l
rev (l ++ l2) ++ [a] = rev l2 ++ rev l ++ [a]

For rewrite we can separate two lemmas to rewrite by a comma.

    rewrite IHl, app_assoc.A: Type
a: A
l, l2: list A
IHl: rev (l ++ l2) = rev l2 ++ rev l
(rev l2 ++ rev l) ++ [a] = (rev l2 ++ rev l) ++ [a] reflexivity.
Qed.

Lemma rev_rev {A} (l : list A) :
  rev (rev l) = l.A: Type
l: list A
rev (rev l) = l
Proof.A: Type
l: list A
rev (rev l) = l
  induction l.A: Type
rev (rev []) = []
A: Type
a: A
l: list A
IHl: rev (rev l) = l
rev (rev (a :: l)) = a :: l all: simpl.A: Type
[] = []
A: Type
a: A
l: list A
IHl: rev (rev l) = l
rev (rev l ++ [a]) = a :: l
  -A: Type
[] = [] reflexivity.
  -A: Type
a: A
l: list A
IHl: rev (rev l) = l
rev (rev l ++ [a]) = a :: l rewrite rev_app_distr.A: Type
a: A
l: list A
IHl: rev (rev l) = l
rev [a] ++ rev (rev l) = a :: l simpl.A: Type
a: A
l: list A
IHl: rev (rev l) = l
a :: rev (rev l) = a :: l rewrite IHl.A: Type
a: A
l: list A
IHl: rev (rev l) = l
a :: l = a :: l reflexivity.
Qed.

The rev defined above is not very smart because it uses concatenation on the right which is expensive. However, it works as a specification for a smarter version using an accumulator.

Fixpoint fast_rev {A} (l : list A) (acc : list A) :=
  match l with
  | [] => acc
  | x :: l => fast_rev l (x :: acc)
  end.

We can show the two behave the same.

Lemma fast_rev_eq {A} (l : list A) :
  fast_rev l nil = rev l.A: Type
l: list A
fast_rev l [] = rev l
Proof.A: Type
l: list A
fast_rev l [] = rev l
  induction l.A: Type
fast_rev [] [] = rev []
A: Type
a: A
l: list A
IHl: fast_rev l [] = rev l
fast_rev (a :: l) [] = rev (a :: l) all: simpl.A: Type
[] = []
A: Type
a: A
l: list A
IHl: fast_rev l [] = rev l
fast_rev l [a] = rev l ++ [a]
  -A: Type
[] = [] reflexivity.
  -A: Type
a: A
l: list A
IHl: fast_rev l [] = rev l
fast_rev l [a] = rev l ++ [a]

We are stuck again, because the acc argument is changed.

Abort.

Lemma fast_rev_eq {A} (l : list A) :
  fast_rev l nil = rev l.A: Type
l: list A
fast_rev l [] = rev l
Proof.A: Type
l: list A
fast_rev l [] = rev l

We prove a more general lemma locally. We're using forall here to introduce a parameter.

  assert (H : forall acc, fast_rev l acc = rev l ++ acc).A: Type
l: list A
forall acc : list A, fast_rev l acc = rev l ++ acc
A: Type
l: list A
H: forall acc : list A, fast_rev l acc = rev l ++ acc
fast_rev l [] = rev l
  {A: Type
l: list A
forall acc : list A, fast_rev l acc = rev l ++ acc induction l as [| a l IHl].A: Type
forall acc : list A, fast_rev [] acc = rev [] ++ acc
A: Type
a: A
l: list A
IHl: forall acc : list A, fast_rev l acc = rev l ++ acc
forall acc : list A, fast_rev (a :: l) acc = rev (a :: l) ++ acc all: simpl.A: Type
forall acc : list A, acc = acc
A: Type
a: A
l: list A
IHl: forall acc : list A, fast_rev l acc = rev l ++ acc
forall acc : list A, fast_rev l (a :: acc) = (rev l ++ [a]) ++ acc all: intros acc.A: Type
acc: list A
acc = acc
A: Type
a: A
l: list A
IHl: forall acc : list A, fast_rev l acc = rev l ++ acc
acc: list A
fast_rev l (a :: acc) = (rev l ++ [a]) ++ acc
    -A: Type
acc: list A
acc = acc reflexivity.
    -A: Type
a: A
l: list A
IHl: forall acc : list A, fast_rev l acc = rev l ++ acc
acc: list A
fast_rev l (a :: acc) = (rev l ++ [a]) ++ acc rewrite IHl.A: Type
a: A
l: list A
IHl: forall acc : list A, fast_rev l acc = rev l ++ acc
acc: list A
rev l ++ a :: acc = (rev l ++ [a]) ++ acc rewrite <- app_assoc.A: Type
a: A
l: list A
IHl: forall acc : list A, fast_rev l acc = rev l ++ acc
acc: list A
rev l ++ a :: acc = rev l ++ [a] ++ acc reflexivity.
  }A: Type
l: list A
H: forall acc : list A, fast_rev l acc = rev l ++ acc
fast_rev l [] = rev l
  rewrite H.A: Type
l: list A
H: forall acc : list A, fast_rev l acc = rev l ++ acc
rev l ++ [] = rev l Search app nil.app_nil_r: forall (A : Type) (l : list A), l ++ [] = l
app_nil_end_deprecated: forall [A : Type] (l : list A), l = l ++ []
List.app_nil_r: forall [A : Type] (l : list A), l ++ [] = l
app_nil_l: forall [A : Type] (l : list A), [] ++ l = l
removelast_last:
  forall [A : Type] (l : list A) (a : A), removelast (l ++ [a]) = l
last_last: forall [A : Type] (l : list A) (a d : A), last (l ++ [a]) d = a
app_cons_not_nil: forall [A : Type] (x y : list A) (a : A), [] <> x ++ a :: y
rev_unit: forall [A : Type] (l : list A) (a : A), rev (l ++ [a]) = a :: rev l
last_length:
  forall [A : Type] (l : list A) (a : A), length (l ++ [a]) = S (length l)
repeat_cons:
  forall [A : Type] (n : nat) (a : A), a :: repeat a n = repeat a n ++ [a]
rev_ind:
  forall [A : Type] (P : list A -> Prop),
  P [] ->
  (forall (x : A) (l : list A), P l -> P (l ++ [x])) ->
  forall l : list A, P l
app_eq_nil:
  forall [A : Type] (l l' : list A), l ++ l' = [] -> l = [] /\ l' = []
seq_S:
  forall len start : nat, seq start (S len) = seq start len ++ [start + len]
removelast_app:
  forall [A : Type] (l : list A) [l' : list A],
  l' <> [] -> removelast (l ++ l') = l ++ removelast l'
app_removelast_last:
  forall [A : Type] [l : list A] (d : A),
  l <> [] -> l = removelast l ++ [last l d]
map_last:
  forall [A B : Type] (f : A -> B) (l : list A) (a : A),
  map f (l ++ [a]) = map f l ++ [f a]
exists_last:
  forall [A : Type] [l : list A],
  l <> [] -> {l' : list A & {a : A | l = l' ++ [a]}}
app_inj_tail:
  forall [A : Type] (x y : list A) (a b : A),
  x ++ [a] = y ++ [b] -> x = y /\ a = b
app_inj_tail_iff:
  forall [A : Type] (x y : list A) (a b : A),
  x ++ [a] = y ++ [b] <-> x = y /\ a = b
elt_eq_unit:
  forall [A : Type] (l1 l2 : list A) (a : A) [b : A],
  l1 ++ a :: l2 = [b] -> a = b /\ l1 = [] /\ l2 = []
Relation_Operators.d_conc:
  forall (A : Set) (leA : A -> A -> Prop) (x y : A) (l : list A),
  Relation_Operators.clos_refl A leA x y ->
  Relation_Operators.Desc A leA (l ++ [y]) ->
  Relation_Operators.Desc A leA ((l ++ [y]) ++ [x])
app_eq_unit:
  forall [A : Type] (x y : list A) [a : A],
  x ++ y = [a] -> x = [] /\ y = [a] \/ x = [a] /\ y = []
app_eq_cons:
  forall [A : Type] (x y : list A) [z : list A] [a : A],
  x ++ y = a :: z ->
  x = [] /\ y = a :: z \/ (exists x' : list A, x = a :: x' /\ z = x' ++ y)
Relation_Operators.Desc_ind:
  forall (A : Set) (leA : A -> A -> Prop) (P : list A -> Prop),
  P [] ->
  (forall x : A, P [x]) ->
  (forall (x y : A) (l : list A),
   Relation_Operators.clos_refl A leA x y ->
   Relation_Operators.Desc A leA (l ++ [y]) ->
   P (l ++ [y]) -> P ((l ++ [y]) ++ [x])) ->
  forall l : list A, Relation_Operators.Desc A leA l -> P l
Relation_Operators.Desc_sind:
  forall (A : Set) (leA : A -> A -> Prop) (P : list A -> SProp),
  P [] ->
  (forall x : A, P [x]) ->
  (forall (x y : A) (l : list A),
   Relation_Operators.clos_refl A leA x y ->
   Relation_Operators.Desc A leA (l ++ [y]) ->
   P (l ++ [y]) -> P ((l ++ [y]) ++ [x])) ->
  forall l : list A, Relation_Operators.Desc A leA l -> P l
A: Type
l: list A
H: forall acc : list A, fast_rev l acc = rev l ++ acc
rev l ++ [] = rev l rewrite app_nil_r.A: Type
l: list A
H: forall acc : list A, fast_rev l acc = rev l ++ acc
rev l = rev l reflexivity.
Qed.

We can prove things in a different way.

Lemma fast_rev_eq_alt {A} (l : list A) :
  fast_rev l nil = rev l.A: Type
l: list A
fast_rev l [] = rev l
Proof.A: Type
l: list A
fast_rev l [] = rev l

We are going to generalise the empty list to any acc. We write @nil A to provide the type argument A explicitly.

  rewrite <- app_nil_r.A: Type
l: list A
fast_rev l [] = rev l ++ [] generalize (@nil A) as acc.A: Type
l: list A
forall acc : list A, fast_rev l acc = rev l ++ acc
  induction l as [| a l IHl].A: Type
forall acc : list A, fast_rev [] acc = rev [] ++ acc
A: Type
a: A
l: list A
IHl: forall acc : list A, fast_rev l acc = rev l ++ acc
forall acc : list A, fast_rev (a :: l) acc = rev (a :: l) ++ acc all: simpl.A: Type
forall acc : list A, acc = acc
A: Type
a: A
l: list A
IHl: forall acc : list A, fast_rev l acc = rev l ++ acc
forall acc : list A, fast_rev l (a :: acc) = (rev l ++ [a]) ++ acc all: intros acc.A: Type
acc: list A
acc = acc
A: Type
a: A
l: list A
IHl: forall acc : list A, fast_rev l acc = rev l ++ acc
acc: list A
fast_rev l (a :: acc) = (rev l ++ [a]) ++ acc
  -A: Type
acc: list A
acc = acc reflexivity.
  -A: Type
a: A
l: list A
IHl: forall acc : list A, fast_rev l acc = rev l ++ acc
acc: list A
fast_rev l (a :: acc) = (rev l ++ [a]) ++ acc rewrite IHl.A: Type
a: A
l: list A
IHl: forall acc : list A, fast_rev l acc = rev l ++ acc
acc: list A
rev l ++ a :: acc = (rev l ++ [a]) ++ acc rewrite <- app_assoc.A: Type
a: A
l: list A
IHl: forall acc : list A, fast_rev l acc = rev l ++ acc
acc: list A
rev l ++ a :: acc = rev l ++ [a] ++ acc reflexivity.
Qed.

Polymorphic iteration

We will now have a look at iter, a function such that iter f n x applies n times the function f, starting with the argument x. For instance iter f 2 x is f (f x).

Fixpoint iter {A : Type} (f : A -> A) (n : nat) (x : A) : A :=
  match n with
  | 0 => x
  | S n' => f (iter f n' x)
  end.

We can show that iterating the successor n times is the same as adding n.

Lemma iter_add n x :
  n + x = iter S n x.n, x: nat
n + x = iter S n x
Proof.n, x: nat
n + x = iter S n x
  induction n as [|n IH].x: nat
0 + x = iter S 0 x
n, x: nat
IH: n + x = iter S n x
S n + x = iter S (S n) x all: simpl.x: nat
x = x
n, x: nat
IH: n + x = iter S n x
S (n + x) = S (iter S n x)
  -x: nat
x = x reflexivity.
  -n, x: nat
IH: n + x = iter S n x
S (n + x) = S (iter S n x) f_equal.n, x: nat
IH: n + x = iter S n x
n + x = iter S n x assumption.
Qed.

Similarly, multiplication is iterated addition.

Lemma iter_mul n x :
  n * x = iter (Nat.add x) n 0.n, x: nat
n * x = iter (Nat.add x) n 0
Proof.n, x: nat
n * x = iter (Nat.add x) n 0
  induction n as [|n IH].x: nat
0 * x = iter (Nat.add x) 0 0
n, x: nat
IH: n * x = iter (Nat.add x) n 0
S n * x = iter (Nat.add x) (S n) 0 all: simpl.x: nat
0 = 0
n, x: nat
IH: n * x = iter (Nat.add x) n 0
x + n * x = x + iter (Nat.add x) n 0
  -x: nat
0 = 0 reflexivity.
  -n, x: nat
IH: n * x = iter (Nat.add x) n 0
x + n * x = x + iter (Nat.add x) n 0 f_equal.n, x: nat
IH: n * x = iter (Nat.add x) n 0
n * x = iter (Nat.add x) n 0 assumption.
Qed.

Mutual inductive types

We will not cover dependent types in a lecture — please have a look at them yourselves.

It is also possible to define several inductive types at the same time. You just combine them with the with keyword.

This way we can define the type of trees mutually with that of forests (which are basically lists of trees).

Inductive tree (A : Type) :=
| nnode : A -> forest A -> tree A

with forest (A : Type) :=
| nnil : forest A
| ncons : tree A -> forest A -> forest A.tree, forest are defined

Scheme tree_ind' := Induction for tree Sort Prop
    with forest_ind' := Induction for forest Sort Prop.tree_ind', forest_ind' are recursively defined
Combined Scheme tree_forest_mutind from tree_ind', forest_ind'.

You can then define mutual definitions over such types by using Fixpoint and the with keyword.

Fixpoint size {A} (t : tree A) {struct t} : nat :=
  match t with
  | nnode _ a l => 1 + size_forest l
  end

with size_forest {A} (l : forest A) {struct l} : nat :=
  match l with
  | nnil _ => 0
  | ncons _ t tl => size t + size_forest tl
  end.size, size_forest are recursively defined (guarded respectively on 2nd,
2nd arguments)

Fixpoint nodes {A} (t : tree A) {struct t} : list A :=
  match t with
  | nnode _ a l => a :: nodes_forest l
  end
with nodes_forest {A} (l : forest A) {struct l} : list A :=
       match l with
       | nnil _ => []
       | ncons _ t tl => nodes t ++ nodes_forest tl
       end.nodes, nodes_forest are recursively defined (guarded respectively on 2nd,
2nd arguments)

Lemma nodes_size {A} (t : tree A) :
  length (nodes t) = size t.A: Type
t: tree A
length (nodes t) = size t
Proof.A: Type
t: tree A
length (nodes t) = size t
  enough
    ((forall t : tree A, length (nodes t) = size t) /\
       (forall f : forest A, length (nodes_forest f) = size_forest f)) as H.A: Type
t: tree A
H: (forall t : tree A, length (nodes t) = size t) /\
(forall f : forest A, length (nodes_forest f) = size_forest f)
length (nodes t) = size t
A: Type
t: tree A
(forall t0 : tree A, length (nodes t0) = size t0) /\
(forall f : forest A, length (nodes_forest f) = size_forest f)
  1: apply H.A: Type
t: tree A
(forall t0 : tree A, length (nodes t0) = size t0) /\
(forall f : forest A, length (nodes_forest f) = size_forest f)
  apply tree_forest_mutind; clear t.A: Type
forall (a : A) (f : forest A),
length (nodes_forest f) = size_forest f ->
length (nodes (nnode A a f)) = size (nnode A a f)
A: Type
length (nodes_forest (nnil A)) = size_forest (nnil A)
A: Type
forall t : tree A,
length (nodes t) = size t ->
forall f : forest A,
length (nodes_forest f) = size_forest f ->
length (nodes_forest (ncons A t f)) = size_forest (ncons A t f)
  -A: Type
forall (a : A) (f : forest A),
length (nodes_forest f) = size_forest f ->
length (nodes (nnode A a f)) = size (nnode A a f) intros a f IH.A: Type
a: A
f: forest A
IH: length (nodes_forest f) = size_forest f
length (nodes (nnode A a f)) = size (nnode A a f)
    cbn.A: Type
a: A
f: forest A
IH: length (nodes_forest f) = size_forest f
S (length (nodes_forest f)) = S (size_forest f) now rewrite IH.
  -A: Type
length (nodes_forest (nnil A)) = size_forest (nnil A) reflexivity.
  -A: Type
forall t : tree A,
length (nodes t) = size t ->
forall f : forest A,
length (nodes_forest f) = size_forest f ->
length (nodes_forest (ncons A t f)) = size_forest (ncons A t f) intros t IHt f IHf.A: Type
t: tree A
IHt: length (nodes t) = size t
f: forest A
IHf: length (nodes_forest f) = size_forest f
length (nodes_forest (ncons A t f)) = size_forest (ncons A t f)
    cbn.A: Type
t: tree A
IHt: length (nodes t) = size t
f: forest A
IHf: length (nodes_forest f) = size_forest f
length (nodes t ++ nodes_forest f) = size t + size_forest f now rewrite length_app, IHt, IHf.
Qed.

Indexed inductive types

We now define a type vector : Type -> nat -> Type where the number is the length. The definition of vectors is not surprising:

Inductive vector (A : Type) : nat -> Type :=
| vnil : vector A 0
| vcons (x : A) (n : nat) (tl : vector A n) : vector A (S n).

In vector A n, A is a parameter, because the whole definition is parametric in A, i.e. A never changes. On the other hand, n is an index, because it changes in the vcons constructor.

There are two ways to ease working with parameters and avoid duplication:

The | notation and sections. Using the first, we can alternatively define vectors as follows, with less duplication of A:

Inductive vector' (A : Type) | : nat -> Type :=
| vnil' : vector' 0
| vcons' (x : A) (n : nat) (tl : vector' n) : vector' (S n).

Sections allow globally fixing variables, such as type variables:

Section fix_A.

  Variable A : Type.

  Inductive vector'' : nat -> Type :=
  | vnil'' : vector'' 0
  | vcons'' (x : A) (n : nat) (tl : vector'' n) : vector'' (S n).

  Check vector''.vector''
     : nat -> Type

End fix_A.

These variables are added as explicit parameters when the section is closed:

Check vector''.vector''
     : Type -> nat -> Type

Rocq generates induction principles for vectors, like it does for e.g. lists. However, to make the induction principle well-typed, the motive P : vector A n -> Prop has to take n as an explicit argument:

Check vector_ind.vector_ind
     : forall (A : Type) (P : forall n : nat, vector A n -> Prop),
       P 0 (vnil A) ->
       (forall (x : A) (n : nat) (tl : vector A n),
        P n tl -> P (S n) (vcons A x n tl)) ->
       forall (n : nat) (v : vector A n), P n v

Try experimenting with writing down the type of an induction principle that looks like this:

forall (A : Type) (forall n : nat) (P : vector A n -> Prop),
 <FILLME> -> <FILLME> -> forall (v : vector A n), P v

It won't be possible!

We can, of course, define recursive functions and do proofs over indexed inductive types, like we are used to:

Fixpoint vmap {A B} (f : A -> B) {n} (v : vector A n) : vector B n :=
  match v with
  | vnil _ => vnil _
  | vcons _ a _ tl => vcons _ (f a) _ (vmap f tl)
  end.

Fixpoint vapp {A}{n}{p} (v:vector A n) (w:vector A p): vector A (n+p) :=
  match v with
  | vnil _ => w
  | vcons _ a _ tl => vcons _ a _ (vapp tl w)
  end.

Lemma vmap_vapp {A B} {n p} (f : A -> B) (v:vector A n) (w:vector A p) :
  vmap f (vapp v w) = vapp (vmap f v) (vmap f w).A, B: Type
n, p: nat
f: A -> B
v: vector A n
w: vector A p
vmap f (vapp v w) = vapp (vmap f v) (vmap f w)
Proof.A, B: Type
n, p: nat
f: A -> B
v: vector A n
w: vector A p
vmap f (vapp v w) = vapp (vmap f v) (vmap f w)
  induction v as [ | a n tl].A, B: Type
p: nat
f: A -> B
w: vector A p
vmap f (vapp (vnil A) w) = vapp (vmap f (vnil A)) (vmap f w)
A, B: Type
p: nat
f: A -> B
a: A
n: nat
tl: vector A n
w: vector A p
IHtl: vmap f (vapp tl w) = vapp (vmap f tl) (vmap f w)
vmap f (vapp (vcons A a n tl) w) = vapp (vmap f (vcons A a n tl)) (vmap f w)
  -A, B: Type
p: nat
f: A -> B
w: vector A p
vmap f (vapp (vnil A) w) = vapp (vmap f (vnil A)) (vmap f w) reflexivity.
  -A, B: Type
p: nat
f: A -> B
a: A
n: nat
tl: vector A n
w: vector A p
IHtl: vmap f (vapp tl w) = vapp (vmap f tl) (vmap f w)
vmap f (vapp (vcons A a n tl) w) = vapp (vmap f (vcons A a n tl)) (vmap f w) simpl.A, B: Type
p: nat
f: A -> B
a: A
n: nat
tl: vector A n
w: vector A p
IHtl: vmap f (vapp tl w) = vapp (vmap f tl) (vmap f w)
vcons B (f a) (n + p) (vmap f (vapp tl w)) =
vcons B (f a) (n + p) (vapp (vmap f tl) (vmap f w))
    rewrite IHtl.A, B: Type
p: nat
f: A -> B
a: A
n: nat
tl: vector A n
w: vector A p
IHtl: vmap f (vapp tl w) = vapp (vmap f tl) (vmap f w)
vcons B (f a) (n + p) (vapp (vmap f tl) (vmap f w)) =
vcons B (f a) (n + p) (vapp (vmap f tl) (vmap f w))
    reflexivity.
Qed.

Dependent pairs

We will cover dependent pairs on Wednesday.

We define the type of dependent pairs, where the second component can depend on the first. We often call those Σ-types (hence the name sigT).

Inductive sigT {A} (B : A -> Type) :=
| existT (a : A) (b : B a) : sigT B.

Arguments existT {A B}.

For instance, we can create a type of pairs, where the first component is always a boolean b, but the second is of type nat when b is true and of type list nat otherwise.

Definition T := sigT (fun (b : bool) => if b then nat else list nat).

We can then create two elements of type T, a pair (true, 17) and a pair (false, [ 90 ; 4 ; 8 ]). This is something you could not do without dependent types (so for instance, not in OCaml).

Definition pair1 : T :=
  existT true 17.

Definition pair2 : T :=
  existT false [ 90 ; 4 ; 8 ].

Important, you should have a look at the induction principle for dependent pairs.

Check sigT_ind.sigT_ind
     : forall (A : Type) (B : A -> Type) (P : sigT B -> Prop),
       (forall (a : A) (b : B a), P (existT a b)) -> forall s : sigT B, P s

Similar to how a function of type A * B -> C is the same as A -> B -> C (which we call currying), we can turn a function of type sigT {A} B -> C to a (dependent) function of type forall (x : A), B x -> C.

Notice that forall can work for dependent functions and not just for propositions.

Definition cur {A} {B : A -> Type} {C} (f : sigT B -> C) :
  forall (x : A), B x -> C :=
  fun a b => f (existT a b).

We can perform the opposite transformation.

Definition car {A} {B : A -> Type} {C} (f : forall x, B x -> C) :
  sigT B -> C :=
  fun p =>
    match p with
    | existT a b => f a b
    end.

And now we can prove that they are indeed inverse of each other.

Lemma car_cur A (B : A -> Type) C (f : sigT B -> C) p :
  car (cur f) p = f p.A: Type
B: A -> Type
C: Type
f: sigT B -> C
p: sigT B
car (cur f) p = f p
Proof.A: Type
B: A -> Type
C: Type
f: sigT B -> C
p: sigT B
car (cur f) p = f p
  destruct p as [a b].A: Type
B: A -> Type
C: Type
f: sigT B -> C
a: A
b: B a
car (cur f) (existT a b) = f (existT a b) reflexivity.
Qed.

The other direction is even simpler, there is nothing to destruct so the proof is direct by reflexivity.

Lemma cur_car A (B : A -> Type) C (f : forall (x : A), B x -> C) a b :
  cur (car f) a b = f a b.A: Type
B: A -> Type
C: Type
f: forall x : A, B x -> C
a: A
b: B a
cur (car f) a b = f a b
Proof.A: Type
B: A -> Type
C: Type
f: forall x : A, B x -> C
a: A
b: B a
cur (car f) a b = f a b
  reflexivity.
Qed.