Start of BasicSyntax code

This commit is contained in:
Adam Chlipala 2015-12-31 15:44:34 -05:00
parent e5898976ab
commit f8945106da
10 changed files with 837 additions and 0 deletions

4
.gitignore vendored
View file

@ -9,3 +9,7 @@
*.blg
*.ilg
*.ind
Makefile.coq
*.glob
*.v.d
*.vo

250
BasicSyntax.v Normal file
View file

@ -0,0 +1,250 @@
(** Formal Reasoning About Programs <http://adam.chlipala.net/frap/>
* Chapter 2: Basic Program Syntax
* Author: Adam Chlipala
* License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *)
Require Import Frap.
Module ArithWithConstants.
Inductive arith : Set :=
| Const (n : nat)
| Plus (e1 e2 : arith)
| Times (e1 e2 : arith).
Example ex1 := Const 42.
Example ex2 := Plus (Const 1) (Times (Const 2) (Const 3)).
Fixpoint size (e : arith) : nat :=
match e with
| Const _ => 1
| Plus e1 e2 => 1 + size e1 + size e2
| Times e1 e2 => 1 + size e1 + size e2
end.
Compute size ex1.
Compute size ex2.
Fixpoint depth (e : arith) : nat :=
match e with
| Const _ => 1
| Plus e1 e2 => 1 + max (depth e1) (depth e2)
| Times e1 e2 => 1 + max (depth e1) (depth e2)
end.
Compute depth ex1.
Compute size ex2.
Theorem depth_le_size : forall e, depth e <= size e.
Proof.
induct e.
simplify.
linear_arithmetic.
simplify.
linear_arithmetic.
simplify.
linear_arithmetic.
Qed.
Theorem depth_le_size_snazzy : forall e, depth e <= size e.
Proof.
induct e; simplify; linear_arithmetic.
Qed.
Fixpoint commuter (e : arith) : arith :=
match e with
| Const _ => e
| Plus e1 e2 => Plus (commuter e2) (commuter e1)
| Times e1 e2 => Times (commuter e2) (commuter e1)
end.
Compute commuter ex1.
Compute commuter ex2.
Theorem size_commuter : forall e, size (commuter e) = size e.
Proof.
induct e; simplify; linear_arithmetic.
Qed.
Theorem depth_commuter : forall e, depth (commuter e) = depth e.
Proof.
induct e; simplify; linear_arithmetic.
Qed.
Theorem commuter_inverse : forall e, commuter (commuter e) = e.
Proof.
induct e; simplify; equality.
Qed.
End ArithWithConstants.
Module ArithWithVariables.
Inductive arith : Set :=
| Const (n : nat)
| Var (x : var)
| Plus (e1 e2 : arith)
| Times (e1 e2 : arith).
Example ex1 := Const 42.
Example ex2 := Plus (Const 1) (Times (Var "x") (Const 3)).
Fixpoint size (e : arith) : nat :=
match e with
| Const _ => 1
| Var _ => 1
| Plus e1 e2 => 1 + size e1 + size e2
| Times e1 e2 => 1 + size e1 + size e2
end.
Compute size ex1.
Compute size ex2.
Fixpoint depth (e : arith) : nat :=
match e with
| Const _ => 1
| Var _ => 1
| Plus e1 e2 => 1 + max (depth e1) (depth e2)
| Times e1 e2 => 1 + max (depth e1) (depth e2)
end.
Compute depth ex1.
Compute size ex2.
Theorem depth_le_size : forall e, depth e <= size e.
Proof.
induct e; simplify; linear_arithmetic.
Qed.
Fixpoint commuter (e : arith) : arith :=
match e with
| Const _ => e
| Var _ => e
| Plus e1 e2 => Plus (commuter e2) (commuter e1)
| Times e1 e2 => Times (commuter e2) (commuter e1)
end.
Compute commuter ex1.
Compute commuter ex2.
Theorem size_commuter : forall e, size (commuter e) = size e.
Proof.
induct e; simplify; linear_arithmetic.
Qed.
Theorem depth_commuter : forall e, depth (commuter e) = depth e.
Proof.
induct e; simplify; linear_arithmetic.
Qed.
Theorem commuter_inverse : forall e, commuter (commuter e) = e.
Proof.
induct e; simplify; equality.
Qed.
Fixpoint substitute (inThis : arith) (replaceThis : var) (withThis : arith) : arith :=
match inThis with
| Const _ => inThis
| Var x => if x ==v replaceThis then withThis else inThis
| Plus e1 e2 => Plus (substitute e1 replaceThis withThis) (substitute e2 replaceThis withThis)
| Times e1 e2 => Times (substitute e1 replaceThis withThis) (substitute e2 replaceThis withThis)
end.
Theorem substitute_depth : forall replaceThis withThis inThis,
depth (substitute inThis replaceThis withThis) <= depth inThis + depth withThis.
Proof.
induct inThis.
simplify.
linear_arithmetic.
simplify.
cases (x ==v replaceThis).
linear_arithmetic.
simplify.
linear_arithmetic.
simplify.
linear_arithmetic.
simplify.
linear_arithmetic.
Qed.
Theorem substitute_depth_snazzy : forall replaceThis withThis inThis,
depth (substitute inThis replaceThis withThis) <= depth inThis + depth withThis.
Proof.
induct inThis; simplify;
try match goal with
| [ |- context[if ?a ==v ?b then _ else _] ] => cases (a ==v b); simplify
end; linear_arithmetic.
Qed.
Theorem substitute_self : forall replaceThis inThis,
substitute inThis replaceThis (Var replaceThis) = inThis.
Proof.
induct inThis; simplify;
try match goal with
| [ |- context[if ?a ==v ?b then _ else _] ] => cases (a ==v b); simplify
end; equality.
Qed.
Theorem substitute_commuter : forall replaceThis withThis inThis,
commuter (substitute inThis replaceThis withThis)
= substitute (commuter inThis) replaceThis (commuter withThis).
Proof.
induct inThis; simplify;
try match goal with
| [ |- context[if ?a ==v ?b then _ else _] ] => cases (a ==v b); simplify
end; equality.
Qed.
Fixpoint constantFold (e : arith) : arith :=
match e with
| Const _ => e
| Var _ => e
| Plus e1 e2 =>
let e1' := constantFold e1 in
let e2' := constantFold e2 in
match e1', e2' with
| Const n1, Const n2 => Const (n1 + n2)
| Const 0, _ => e2'
| _, Const 0 => e1'
| _, _ => Plus e1' e2'
end
| Times e1 e2 =>
let e1' := constantFold e1 in
let e2' := constantFold e2 in
match e1', e2' with
| Const n1, Const n2 => Const (n1 * n2)
| Const 1, _ => e2'
| _, Const 1 => e1'
| Const 0, _ => Const 0
| _, Const 0 => Const 0
| _, _ => Times e1' e2'
end
end.
Theorem size_constantFold : forall e, size (constantFold e) <= size e.
Proof.
induct e; simplify;
repeat match goal with
| [ |- context[match ?E with _ => _ end] ] => cases E; simplify
end; linear_arithmetic.
Qed.
Theorem commuter_constantFold : forall e, commuter (constantFold e) = constantFold (commuter e).
Proof.
induct e; simplify;
repeat match goal with
| [ |- context[match ?E with _ => _ end] ] => cases E; simplify
| [ H : ?f _ = ?f _ |- _ ] => invert H
| [ |- ?f _ = ?f _ ] => f_equal
end; equality || linear_arithmetic || ring.
Qed.
End ArithWithVariables.

70
Frap.v Normal file
View file

@ -0,0 +1,70 @@
Require Import String Arith Omega Program Sets Relations Map Var Invariant.
Export String Arith Sets Relations Map Var Invariant.
Require Import List.
Export ListNotations.
Open Scope string_scope.
Ltac inductN n :=
match goal with
| [ |- forall x : ?E, _ ] =>
match type of E with
| Prop =>
let H := fresh in intro H;
match n with
| 1 => dependent induction H
| S ?n' => inductN n'
end
| _ => intro; inductN n
end
end.
Ltac induct e := inductN e || dependent induction e.
Ltac invert' H := inversion H; clear H; subst.
Ltac invertN n :=
match goal with
| [ |- forall x : ?E, _ ] =>
match type of E with
| Prop =>
let H := fresh in intro H;
match n with
| 1 => invert' H
| S ?n' => invertN n'
end
| _ => intro; invertN n
end
end.
Ltac invert e := invertN e || invert' e.
Ltac invert0 e := invert e; fail.
Ltac invert1 e := invert0 e || (invert e; []).
Ltac invert2 e := invert1 e || (invert e; [|]).
Ltac simplify := simpl in *.
Ltac linear_arithmetic :=
repeat match goal with
| [ |- context[max ?a ?b] ] =>
let Heq := fresh "Heq" in destruct (Max.max_spec a b) as [[? Heq] | [? Heq]];
rewrite Heq in *; clear Heq
| [ _ : context[max ?a ?b] |- _ ] =>
let Heq := fresh "Heq" in destruct (Max.max_spec a b) as [[? Heq] | [? Heq]];
rewrite Heq in *; clear Heq
| [ |- context[min ?a ?b] ] =>
let Heq := fresh "Heq" in destruct (Min.min_spec a b) as [[? Heq] | [? Heq]];
rewrite Heq in *; clear Heq
| [ _ : context[min ?a ?b] |- _ ] =>
let Heq := fresh "Heq" in destruct (Min.min_spec a b) as [[? Heq] | [? Heq]];
rewrite Heq in *; clear Heq
end; omega.
Ltac equality := congruence.
Ltac cases E :=
(is_var E; destruct E)
|| match type of E with
| {_} + {_} => destruct E
| _ => let Heq := fresh "Heq" in destruct E eqn:Heq
end.

30
Invariant.v Normal file
View file

@ -0,0 +1,30 @@
Require Import Relations.
Set Implicit Arguments.
Section Invariant.
Variable state : Type.
Variable step : state -> state -> Prop.
Variable invariant : state -> Prop.
Hint Constructors trc.
Definition safe (s : state) :=
forall s', step^* s s' -> invariant s'.
Variable s0 : state.
Hypothesis Hinitial : invariant s0.
Hypothesis Hstep : forall s s', invariant s -> step s s' -> invariant s'.
Lemma safety : safe s0.
Proof.
generalize dependent s0.
unfold safe.
induction 2; eauto.
Qed.
End Invariant.
Hint Resolve safety.

View file

@ -1,6 +1,20 @@
.PHONY: all coq
all: frap.pdf coq
frap.pdf: frap.tex Makefile
pdflatex frap
pdflatex frap
makeindex frap
pdflatex frap
pdflatex frap
coq: Makefile.coq
$(MAKE) -f Makefile.coq
Makefile.coq: Makefile _CoqProject *.v
coq_makefile -f _CoqProject -o Makefile.coq
clean:: Makefile.coq
$(MAKE) -f Makefile.coq clean
rm -f Makefile.coq

216
Map.v Normal file
View file

@ -0,0 +1,216 @@
Require Import Classical Sets ClassicalEpsilon FunctionalExtensionality.
Set Implicit Arguments.
Module Type S.
Parameter map : Type -> Type -> Type.
Parameter empty : forall A B, map A B.
Parameter add : forall A B, map A B -> A -> B -> map A B.
Parameter join : forall A B, map A B -> map A B -> map A B.
Parameter lookup : forall A B, map A B -> A -> option B.
Parameter includes : forall A B, map A B -> map A B -> Prop.
Notation "$0" := (empty _ _).
Notation "m $+ ( k , v )" := (add m k v) (at level 50, left associativity).
Infix "$++" := join (at level 50, left associativity).
Infix "$?" := lookup (at level 50, no associativity).
Infix "$<=" := includes (at level 90).
Parameter dom : forall A B, map A B -> set A.
Axiom map_ext : forall A B (m1 m2 : map A B),
(forall k, m1 $? k = m2 $? k)
-> m1 = m2.
Axiom lookup_empty : forall A B k, empty A B $? k = None.
Axiom includes_lookup : forall A B (m m' : map A B) k v,
m $? k = Some v
-> m $<= m'
-> lookup m' k = Some v.
Axiom includes_add : forall A B (m m' : map A B) k v,
m $<= m'
-> add m k v $<= add m' k v.
Axiom lookup_add_eq : forall A B (m : map A B) k v,
add m k v $? k = Some v.
Axiom lookup_add_ne : forall A B (m : map A B) k k' v,
k' <> k
-> add m k v $? k' = m $? k'.
Axiom lookup_join1 : forall A B (m1 m2 : map A B) k,
k \in dom m1
-> (m1 $++ m2) $? k = m1 $? k.
Axiom lookup_join2 : forall A B (m1 m2 : map A B) k,
~k \in dom m1
-> (m1 $++ m2) $? k = m2 $? k.
Axiom join_comm : forall A B (m1 m2 : map A B),
dom m1 \cap dom m2 = {}
-> m1 $++ m2 = m2 $++ m1.
Axiom join_assoc : forall A B (m1 m2 m3 : map A B),
(m1 $++ m2) $++ m3 = m1 $++ (m2 $++ m3).
Axiom empty_includes : forall A B (m : map A B), empty A B $<= m.
Axiom dom_empty : forall A B, dom (empty A B) = {}.
Axiom dom_add : forall A B (m : map A B) (k : A) (v : B),
dom (add m k v) = {k} \cup dom m.
Hint Extern 1 => match goal with
| [ H : lookup (empty _ _) _ = Some _ |- _ ] =>
rewrite lookup_empty in H; discriminate
end.
Hint Resolve includes_lookup includes_add empty_includes.
Hint Rewrite lookup_add_eq lookup_add_ne using congruence.
Ltac maps_equal :=
apply map_ext; intros;
repeat (subst; autorewrite with core; try reflexivity;
match goal with
| [ |- context[lookup (add _ ?k _) ?k' ] ] => destruct (classic (k = k')); subst
end).
Hint Extern 3 (_ = _) => maps_equal.
End S.
Module M : S.
Definition map (A B : Type) := A -> option B.
Definition empty A B : map A B := fun _ => None.
Section decide.
Variable P : Prop.
Lemma decided : inhabited (sum P (~P)).
Proof.
destruct (classic P).
constructor; exact (inl _ H).
constructor; exact (inr _ H).
Qed.
Definition decide : sum P (~P) :=
epsilon decided (fun _ => True).
End decide.
Definition add A B (m : map A B) (k : A) (v : B) : map A B :=
fun k' => if decide (k' = k) then Some v else m k'.
Definition join A B (m1 m2 : map A B) : map A B :=
fun k => match m1 k with
| None => m2 k
| x => x
end.
Definition lookup A B (m : map A B) (k : A) := m k.
Definition includes A B (m1 m2 : map A B) :=
forall k v, m1 k = Some v -> m2 k = Some v.
Definition dom A B (m : map A B) : set A := fun x => m x <> None.
Theorem map_ext : forall A B (m1 m2 : map A B),
(forall k, lookup m1 k = lookup m2 k)
-> m1 = m2.
Proof.
intros; extensionality k; auto.
Qed.
Theorem lookup_empty : forall A B (k : A), lookup (empty B) k = None.
Proof.
auto.
Qed.
Theorem includes_lookup : forall A B (m m' : map A B) k v,
lookup m k = Some v
-> includes m m'
-> lookup m' k = Some v.
Proof.
auto.
Qed.
Theorem includes_add : forall A B (m m' : map A B) k v,
includes m m'
-> includes (add m k v) (add m' k v).
Proof.
unfold includes, add; intuition.
destruct (decide (k0 = k)); auto.
Qed.
Theorem lookup_add_eq : forall A B (m : map A B) k v,
lookup (add m k v) k = Some v.
Proof.
unfold lookup, add; intuition.
destruct (decide (k = k)); tauto.
Qed.
Theorem lookup_add_ne : forall A B (m : map A B) k k' v,
k' <> k
-> lookup (add m k v) k' = lookup m k'.
Proof.
unfold lookup, add; intuition.
destruct (decide (k' = k)); intuition.
Qed.
Theorem lookup_join1 : forall A B (m1 m2 : map A B) k,
k \in dom m1
-> lookup (join m1 m2) k = lookup m1 k.
Proof.
unfold lookup, join, dom, In; intros.
destruct (m1 k); congruence.
Qed.
Theorem lookup_join2 : forall A B (m1 m2 : map A B) k,
~k \in dom m1
-> lookup (join m1 m2) k = lookup m2 k.
Proof.
unfold lookup, join, dom, In; intros.
destruct (m1 k); try congruence.
exfalso; apply H; congruence.
Qed.
Theorem join_comm : forall A B (m1 m2 : map A B),
dom m1 \cap dom m2 = {}
-> join m1 m2 = join m2 m1.
Proof.
intros; apply map_ext; unfold join, lookup; intros.
apply (f_equal (fun f => f k)) in H.
unfold dom, intersection, constant in H; simpl in H.
destruct (m1 k), (m2 k); auto.
exfalso; rewrite <- H.
intuition congruence.
Qed.
Theorem join_assoc : forall A B (m1 m2 m3 : map A B),
join (join m1 m2) m3 = join m1 (join m2 m3).
Proof.
intros; apply map_ext; unfold join, lookup; intros.
destruct (m1 k); auto.
Qed.
Theorem empty_includes : forall A B (m : map A B), includes (empty (A := A) B) m.
Proof.
unfold includes, empty; intuition congruence.
Qed.
Theorem dom_empty : forall A B, dom (empty (A := A) B) = {}.
Proof.
unfold dom, empty; intros; sets idtac.
Qed.
Theorem dom_add : forall A B (m : map A B) (k : A) (v : B),
dom (add m k v) = {k} \cup dom m.
Proof.
unfold dom, add; simpl; intros.
sets ltac:(simpl in *; try match goal with
| [ _ : context[if ?E then _ else _] |- _ ] => destruct E
end; intuition congruence).
Qed.
End M.
Export M.

122
Relations.v Normal file
View file

@ -0,0 +1,122 @@
Set Implicit Arguments.
Section trc.
Variable A : Type.
Variable R : A -> A -> Prop.
Inductive trc : A -> A -> Prop :=
| TrcRefl : forall x, trc x x
| TrcFront : forall x y z,
R x y
-> trc y z
-> trc x z.
Hint Constructors trc.
Theorem trc_trans : forall x y, trc x y
-> forall z, trc y z
-> trc x z.
Proof.
induction 1; eauto.
Qed.
Hint Resolve trc_trans.
Inductive trcEnd : A -> A -> Prop :=
| TrcEndRefl : forall x, trcEnd x x
| TrcBack : forall x y z,
trcEnd x y
-> R y z
-> trcEnd x z.
Hint Constructors trcEnd.
Lemma TrcFront' : forall x y z,
R x y
-> trcEnd y z
-> trcEnd x z.
Proof.
induction 2; eauto.
Qed.
Hint Resolve TrcFront'.
Theorem trc_trcEnd : forall x y, trc x y
-> trcEnd x y.
Proof.
induction 1; eauto.
Qed.
Hint Resolve trc_trcEnd.
Lemma TrcBack' : forall x y z,
trc x y
-> R y z
-> trc x z.
Proof.
induction 1; eauto.
Qed.
Hint Resolve TrcBack'.
Theorem trcEnd_trans : forall x y, trcEnd x y
-> forall z, trcEnd y z
-> trcEnd x z.
Proof.
induction 1; eauto.
Qed.
Hint Resolve trcEnd_trans.
Theorem trcEnd_trc : forall x y, trcEnd x y
-> trc x y.
Proof.
induction 1; eauto.
Qed.
Hint Resolve trcEnd_trc.
Inductive trcLiteral : A -> A -> Prop :=
| TrcLiteralRefl : forall x, trcLiteral x x
| TrcTrans : forall x y z, trcLiteral x y
-> trcLiteral y z
-> trcLiteral x z
| TrcInclude : forall x y, R x y
-> trcLiteral x y.
Hint Constructors trcLiteral.
Theorem trc_trcLiteral : forall x y, trc x y
-> trcLiteral x y.
Proof.
induction 1; eauto.
Qed.
Theorem trcLiteral_trc : forall x y, trcLiteral x y
-> trc x y.
Proof.
induction 1; eauto.
Qed.
Hint Resolve trc_trcLiteral trcLiteral_trc.
Theorem trcEnd_trcLiteral : forall x y, trcEnd x y
-> trcLiteral x y.
Proof.
induction 1; eauto.
Qed.
Theorem trcLiteral_trcEnd : forall x y, trcLiteral x y
-> trcEnd x y.
Proof.
induction 1; eauto.
Qed.
Hint Resolve trcEnd_trcLiteral trcLiteral_trcEnd.
End trc.
Notation "R ^*" := (trc R) (at level 0).
Notation "*^ R" := (trcEnd R) (at level 0).
Hint Constructors trc.

117
Sets.v Normal file
View file

@ -0,0 +1,117 @@
Require Import Classical FunctionalExtensionality List.
Set Implicit Arguments.
Axiom prop_ext : forall P Q : Prop,
(P <-> Q) -> P = Q.
Section set.
Variable A : Type.
Definition set := A -> Prop.
Definition In (x : A) (s : set) := s x.
Definition constant (ls : list A) : set := fun x => List.In x ls.
Definition universe : set := fun _ => True.
Definition check (P : Prop) : set := fun _ => P.
Definition union (s1 s2 : set) : set := fun x => s1 x \/ s2 x.
Definition intersection (s1 s2 : set) : set := fun x => s1 x /\ s2 x.
Definition complement (s : set) : set := fun x => ~s x.
Definition subseteq (s1 s2 : set) := forall x, s1 x -> s2 x.
Definition subset (s1 s2 : set) := subseteq s1 s2 /\ ~subseteq s2 s1.
Definition scomp (P : A -> Prop) : set := P.
Theorem sets_equal : forall s1 s2 : set, (forall x, s1 x <-> s2 x) -> s1 = s2.
Proof.
intros.
apply functional_extensionality; intros.
apply prop_ext; auto.
Qed.
End set.
Infix "\in" := In (at level 70).
Notation "{ }" := (constant nil).
Notation "{ x1 , .. , xN }" := (constant (cons x1 (.. (cons xN nil) ..))).
Notation "[ P ]" := (check P).
Infix "\cup" := union (at level 40).
Infix "\cap" := intersection (at level 40).
Infix "\subseteq" := subseteq (at level 70).
Infix "\subset" := subset (at level 70).
Notation "[ x | P ]" := (scomp (fun x => P)).
Ltac sets' tac :=
unfold In, constant, universe, check, union, intersection, complement, subseteq, subset, scomp in *;
tauto || intuition tac.
Ltac sets tac :=
try match goal with
| [ |- @eq (set _) _ _ ] => apply sets_equal; intro; split
end; sets' tac.
(** * Some of the usual properties of set operations *)
Section properties.
Variable A : Type.
Variable x : A.
Variables s1 s2 s3 : set A.
Theorem union_comm : s1 \cup s2 = s2 \cup s1.
Proof.
sets idtac.
Qed.
Theorem union_assoc : (s1 \cup s2) \cup s3 = s1 \cup (s2 \cup s3).
Proof.
sets idtac.
Qed.
Theorem intersection_comm : s1 \cap s2 = s2 \cap s1.
Proof.
sets idtac.
Qed.
Theorem intersection_assoc : (s1 \cap s2) \cap s3 = s1 \cap (s2 \cap s3).
Proof.
sets idtac.
Qed.
Theorem not_union : complement (s1 \cup s2) = complement s1 \cap complement s2.
Proof.
sets idtac.
Qed.
Theorem not_intersection : complement (s1 \cap s2) = complement s1 \cup complement s2.
Proof.
sets idtac.
Qed.
Theorem subseteq_refl : s1 \subseteq s1.
Proof.
unfold subseteq; eauto.
Qed.
Theorem subseteq_In : s1 \subseteq s2 -> x \in s1 -> x \in s2.
Proof.
unfold subseteq, In; eauto.
Qed.
Theorem cap_split : forall (P1 P2 : A -> Prop),
(forall s, P1 s \/ P2 s)
-> s1 \cap [s | P1 s] \subseteq s2
-> s1 \cap [s | P2 s] \subseteq s3
-> s1 \subseteq (s2 \cap [s | P1 s]) \cup (s3 \cap [s | P2 s]).
Proof.
intros; sets eauto.
specialize (H x0).
specialize (H0 x0).
specialize (H1 x0).
tauto.
Qed.
End properties.
Hint Resolve subseteq_refl subseteq_In.

7
Var.v Normal file
View file

@ -0,0 +1,7 @@
Require Import String.
Definition var := string.
Definition var_eq : forall x y : var, {x = y} + {x <> y} := string_dec.
Infix "==v" := var_eq (no associativity, at level 50).

7
_CoqProject Normal file
View file

@ -0,0 +1,7 @@
-R . Frap
Map.v
Var.v
Sets.v
Relations.v
Frap.v
BasicSyntax.v