- Transition to Processing
- Primitive Operations
- Algorithms
- Variables
- Debugging in Processing
- Conditions
- Loops
- Functions
- Scope
- Compound Data
- Reference Semantics
- Refactoring
- Program Design
- Transition to Java
- Debugging in Java
- Unit Testing
- Classes - Writing your own Types
- Classes - Copying objects
- Classes - Functions inside objects
- Classes - Composition
- Classes - Array of objects
- Classes - Class holding array(s)
- Recursion - What goes on during a function call
- Recursion
- Recursion with String data
- Tail-optimized recursion
- Recursion with arrays
- Lists
- Iteration
- List of Lists
- Custom-built ArrayList
- Recursive data structures - 1
- Recursive data structures - 2
- Searching

- Logic and Proofs
- Relations
- Mathematical Functions
- Matrices
- Binary Numbers
- Trigonomtry
- Finite State Machines
- Turing Machines
- Counting - Inclusion/Exclusion
- Graph Algorithms

- Algorithm Efficiency
- Algorithm Correctness
- Trees
- Heaps, Stack, and Queues
- Maps and Hashtables
- Graphs and Graph Algorithms
- Advanced Trees and Computability

- Command line control
- Transition to C
- Pointers
- Memory Allocation
- IO
- Number representations
- Assembly Programming
- Structs and Unions
- How memory works
- Virtual Memory

- Version Control with Git
- Inheritance and Overloading
- Generics
- Exceptions
- Lambda Expressions
- Design Patterns
- Concepts of Concurrency
- Concurrency: Object Locks
- Modern Concurrency

- System Models
- Naming and Distributed File Systems
- Synchronisation and Concurrency
- Fault Tolerance and Security
- Clusters and Grids
- Virtualisation
- Data Centers
- Mobile Computing

- Transition to Scala
- Functional Programming
- Syntax Analysis
- Name Analysis
- Type Analysis
- Transformation and Compilation
- Control Abstraction
- Implementing Data Abstraction
- Language Runtimes

- Transition to Coq
- Proof by Induction, Structured Data
- Polymorphism and Higher-Order Functions
- More Basic Tactics
- Logical Reasoning in Proof Assistants
- Inductive Propositions
- Maps
- An Imperative Programming Language
- Program Equivalence
- Hoare Logic
- Small-Step Operational Semantics
- Simply-typed Lambda Calculus

This material is taken verbatim from Software Foundations V4.0

Copyright (c) 2016 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

Grab the Coq source file Maps.v

Require Import Coq.Arith.Arith.

Require Import Coq.Bool.Bool.

Require Import Coq.Logic.FunctionalExtensionality.

Documentation for the standard library can be found at
http://coq.inria.fr/library/.
The SearchAbout command is a good way to look for theorems
involving objects of specific types.

Inductive id : Type :=

| Id : nat → id.

Definition beq_id id

match id

| Id n

end.

Theorem beq_id_refl : ∀id, true = beq_id id id.

The following useful property of beq_id follows from an
analogous lemma about numbers:

Theorem beq_id_true_iff : ∀id

beq_id id

Proof.

intros [n_{1}] [n_{2}].

unfold beq_id.

rewrite beq_nat_true_iff.

split.

- (* -> *) intros H. rewrite H. reflexivity.

- (* <- *) intros H. inversion H. reflexivity.

Qed.

intros [n

unfold beq_id.

rewrite beq_nat_true_iff.

split.

- (* -> *) intros H. rewrite H. reflexivity.

- (* <- *) intros H. inversion H. reflexivity.

Qed.

Similarly:

This useful variant follows just by rewriting:

Intuitively, a total map over an element type A *is* just a
function that can be used to look up ids, yielding As.
The function t_empty yields an empty total map, given a default
element; this map always returns the default element when applied
to any id.

More interesting is the update function, which (as before) takes
a map m, a key x, and a value v and returns a new map that
takes x to v and takes every other key to whatever m does.

Definition t_update {A:Type} (m : total_map A)

(x : id) (v : A) :=

fun x' ⇒ if beq_id x x' then v else m x'.

This definition is a nice example of higher-order programming.
The t_update function takes a *function* m and yields a new
function fun x' ⇒ ... that behaves like the desired map.
For example, we can build a map taking ids to bools, where Id
3 is mapped to true and every other key is mapped to false,
like this:

This completes the definition of total maps. Note that we don't
need to define a find operation because it is just function
application!

Example update_example1 : examplemap (Id 0) = false.

Proof. reflexivity. Qed.

Example update_example2 : examplemap (Id 1) = false.

Proof. reflexivity. Qed.

Example update_example3 : examplemap (Id 2) = false.

Proof. reflexivity. Qed.

Example update_example4 : examplemap (Id 3) = true.

Proof. reflexivity. Qed.

To use maps in later chapters, we'll need several fundamental
facts about how they behave. Even if you don't work the following
exercises, make sure you thoroughly understand the statements of
the lemmas! (Some of the proofs require the functional
extensionality axiom, which is discussed in the Logic
chapter and included in the Coq standard library.)
#### Exercise: 1 star, optional (t_apply_empty)

First, the empty map returns its default element for all keys:

☐
#### Exercise: 2 stars, optional (t_update_eq)

Next, if we update a map m at a key x with a new value v
and then look up x in the map resulting from the update, we
get back v:

Lemma t_update_eq : ∀A (m: total_map A) x v,

(t_update m x v) x = v.

Proof.

(* FILL IN HERE *) Admitted.

☐
#### Exercise: 2 stars, optional (t_update_neq)

On the other hand, if we update a map m at a key x_{1} and then
look up a *different* key x_{2} in the resulting map, we get the
same result that m would have given:

Theorem t_update_neq : ∀(X:Type) v x

(m : total_map X),

x

(t_update m x

Proof.

(* FILL IN HERE *) Admitted.

☐
#### Exercise: 2 stars, optional (t_update_shadow)

If we update a map m at a key x with a value v_{1} and then
update again with the same key x and another value v_{2}, the
resulting map behaves the same (gives the same result when applied
to any key) as the simpler map obtained by performing just
the second update on m:

Lemma t_update_shadow : ∀A (m: total_map A) v

t_update (t_update m x v

= t_update m x v

Proof.

(* FILL IN HERE *) Admitted.

☐
For the final two lemmas about total maps, it's convenient to use
the reflection idioms introduced in chapter IndProp. We begin
by proving a fundamental *reflection lemma* relating the equality
proposition on ids with the boolean function beq_id.
#### Exercise: 2 stars (beq_idP)

Use the proof of beq_natP in chapter IndProp as a template to
prove the following:

☐
Now, given ids x_{1} and x_{2}, we can use the destruct (beq_idP
x_{1} x_{2}) to simultaneously perform case analysis on the result of
beq_id x_{1} x_{2} and generate hypotheses about the equality (in the
sense of =) of x_{1} and x_{2}.
#### Exercise: 2 stars (t_update_same)

Using the example in chapter IndProp as a template, use
beq_idP to prove the following theorem, which states that if we
update a map to assign key x the same value as it already has in
m, then the result is equal to m:

Theorem t_update_same : ∀X x (m : total_map X),

t_update m x (m x) = m.

Proof.

(* FILL IN HERE *) Admitted.

☐
#### Exercise: 3 stars, recommended (t_update_permute)

Use beq_idP to prove one final property of the update
function: If we update a map m at two distinct keys, it doesn't
matter in which order we do the updates.

Theorem t_update_permute : ∀(X:Type) v

(m : total_map X),

x

(t_update (t_update m x

= (t_update (t_update m x

Proof.

(* FILL IN HERE *) Admitted.

☐

Definition partial_map (A:Type) := total_map (option A).

Definition empty {A:Type} : partial_map A :=

t_empty None.

Definition update {A:Type} (m : partial_map A)

(x : id) (v : A) :=

t_update m x (Some v).

We can now lift all of the basic lemmas about total maps to
partial maps.

Lemma apply_empty : ∀A x, @empty A x = None.

Lemma update_eq : ∀A (m: partial_map A) x v,

(update m x v) x = Some v.

Theorem update_neq : ∀(X:Type) v x

(m : partial_map X),

x

(update m x

Lemma update_shadow : ∀A (m: partial_map A) v

update (update m x v

Theorem update_same : ∀X v x (m : partial_map X),

m x = Some v →

update m x v = m.

Theorem update_permute : ∀(X:Type) v

(m : partial_map X),

x

(update (update m x

= (update (update m x