From f8945106daa63f0d5923eca495b2b645c8139ebd Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 31 Dec 2015 15:44:34 -0500 Subject: [PATCH] Start of BasicSyntax code --- .gitignore | 4 + BasicSyntax.v | 250 ++++++++++++++++++++++++++++++++++++++++++++++++++ Frap.v | 70 ++++++++++++++ Invariant.v | 30 ++++++ Makefile | 14 +++ Map.v | 216 +++++++++++++++++++++++++++++++++++++++++++ Relations.v | 122 ++++++++++++++++++++++++ Sets.v | 117 +++++++++++++++++++++++ Var.v | 7 ++ _CoqProject | 7 ++ 10 files changed, 837 insertions(+) create mode 100644 BasicSyntax.v create mode 100644 Frap.v create mode 100644 Invariant.v create mode 100644 Map.v create mode 100644 Relations.v create mode 100644 Sets.v create mode 100644 Var.v create mode 100644 _CoqProject diff --git a/.gitignore b/.gitignore index 2b6f3f3..23c68e5 100644 --- a/.gitignore +++ b/.gitignore @@ -9,3 +9,7 @@ *.blg *.ilg *.ind +Makefile.coq +*.glob +*.v.d +*.vo diff --git a/BasicSyntax.v b/BasicSyntax.v new file mode 100644 index 0000000..ed82e3f --- /dev/null +++ b/BasicSyntax.v @@ -0,0 +1,250 @@ +(** Formal Reasoning About Programs + * 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. diff --git a/Frap.v b/Frap.v new file mode 100644 index 0000000..c0a7a78 --- /dev/null +++ b/Frap.v @@ -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. diff --git a/Invariant.v b/Invariant.v new file mode 100644 index 0000000..0ff66bb --- /dev/null +++ b/Invariant.v @@ -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. diff --git a/Makefile b/Makefile index f96a0a0..79ef23d 100644 --- a/Makefile +++ b/Makefile @@ -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 diff --git a/Map.v b/Map.v new file mode 100644 index 0000000..77f1aea --- /dev/null +++ b/Map.v @@ -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. diff --git a/Relations.v b/Relations.v new file mode 100644 index 0000000..9454813 --- /dev/null +++ b/Relations.v @@ -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. diff --git a/Sets.v b/Sets.v new file mode 100644 index 0000000..7df06d3 --- /dev/null +++ b/Sets.v @@ -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. diff --git a/Var.v b/Var.v new file mode 100644 index 0000000..b042217 --- /dev/null +++ b/Var.v @@ -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). diff --git a/_CoqProject b/_CoqProject new file mode 100644 index 0000000..9604142 --- /dev/null +++ b/_CoqProject @@ -0,0 +1,7 @@ +-R . Frap +Map.v +Var.v +Sets.v +Relations.v +Frap.v +BasicSyntax.v