mirror of
https://github.com/achlipala/frap.git
synced 2024-11-12 17:17:50 +00:00
SubsetTypes
This commit is contained in:
parent
88df5601f5
commit
c5600db874
9 changed files with 1038 additions and 390 deletions
374
Frap.v
374
Frap.v
|
@ -1,373 +1,3 @@
|
|||
Require Import Eqdep String Arith Omega Program Sets Relations Map Var Invariant Bool ModelCheck.
|
||||
Export String Arith Sets Relations Map Var Invariant Bool ModelCheck.
|
||||
Require Import List.
|
||||
Export List ListNotations.
|
||||
Open Scope string_scope.
|
||||
Open Scope list_scope.
|
||||
Require Export FrapWithoutSets.
|
||||
|
||||
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 same_structure x y :=
|
||||
match x with
|
||||
| ?f ?a1 ?b1 ?c1 ?d1 =>
|
||||
match y with
|
||||
| f ?a2 ?b2 ?c2 ?d2 => same_structure a1 a2; same_structure b1 b2; same_structure c1 c2; same_structure d1 d2
|
||||
| _ => fail 2
|
||||
end
|
||||
| ?f ?a1 ?b1 ?c1 =>
|
||||
match y with
|
||||
| f ?a2 ?b2 ?c2 => same_structure a1 a2; same_structure b1 b2; same_structure c1 c2
|
||||
| _ => fail 2
|
||||
end
|
||||
| ?f ?a1 ?b1 =>
|
||||
match y with
|
||||
| f ?a2 ?b2 => same_structure a1 a2; same_structure b1 b2
|
||||
| _ => fail 2
|
||||
end
|
||||
| ?f ?a1 =>
|
||||
match y with
|
||||
| f ?a2 => same_structure a1 a2
|
||||
| _ => fail 2
|
||||
end
|
||||
| _ =>
|
||||
match y with
|
||||
| ?f ?a1 ?b1 ?c1 ?d1 =>
|
||||
match x with
|
||||
| f ?a2 ?b2 ?c2 ?d2 => same_structure a1 a2; same_structure b1 b2; same_structure c1 c2; same_structure d1 d2
|
||||
| _ => fail 2
|
||||
end
|
||||
| ?f ?a1 ?b1 ?c1 =>
|
||||
match x with
|
||||
| f ?a2 ?b2 ?c2 => same_structure a1 a2; same_structure b1 b2; same_structure c1 c2
|
||||
| _ => fail 2
|
||||
end
|
||||
| ?f ?a1 ?b1 =>
|
||||
match x with
|
||||
| f ?a2 ?b2 => same_structure a1 a2; same_structure b1 b2
|
||||
| _ => fail 2
|
||||
end
|
||||
| ?f ?a1 =>
|
||||
match x with
|
||||
| f ?a2 => same_structure a1 a2
|
||||
| _ => fail 2
|
||||
end
|
||||
| _ => idtac
|
||||
end
|
||||
end.
|
||||
|
||||
Ltac instantiate_obvious1 H :=
|
||||
match type of H with
|
||||
| _ ++ _ = _ ++ _ -> _ => fail 1
|
||||
| ?x = ?y -> _ =>
|
||||
(same_structure x y; specialize (H eq_refl))
|
||||
|| (has_evar (x, y); fail 3)
|
||||
| JMeq.JMeq ?x ?y -> _ =>
|
||||
(same_structure x y; specialize (H JMeq.JMeq_refl))
|
||||
|| (has_evar (x, y); fail 3)
|
||||
| forall x : ?T, _ =>
|
||||
match type of T with
|
||||
| Prop => fail 1
|
||||
| _ =>
|
||||
let x' := fresh x in
|
||||
evar (x' : T);
|
||||
let x'' := eval unfold x' in x' in specialize (H x''); clear x';
|
||||
instantiate_obvious1 H
|
||||
end
|
||||
end.
|
||||
|
||||
Ltac instantiate_obvious H :=
|
||||
match type of H with
|
||||
| context[@eq string _ _] => idtac
|
||||
| _ => repeat instantiate_obvious1 H
|
||||
end.
|
||||
|
||||
Ltac instantiate_obviouses :=
|
||||
repeat match goal with
|
||||
| [ H : _ |- _ ] => instantiate_obvious H
|
||||
end.
|
||||
|
||||
Ltac induct e := (inductN e || dependent induction e); instantiate_obviouses.
|
||||
|
||||
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 maps_neq :=
|
||||
match goal with
|
||||
| [ H : ?m1 = ?m2 |- _ ] =>
|
||||
let rec recur E :=
|
||||
match E with
|
||||
| ?E' $+ (?k, _) =>
|
||||
(apply (f_equal (fun m => m $? k)) in H; simpl in *; autorewrite with core in *; simpl in *; congruence)
|
||||
|| recur E'
|
||||
end in
|
||||
recur m1 || recur m2
|
||||
end.
|
||||
|
||||
Ltac fancy_neq :=
|
||||
repeat match goal with
|
||||
| _ => maps_neq
|
||||
| [ H : @eq (nat -> _) _ _ |- _ ] => apply (f_equal (fun f => f 0)) in H
|
||||
| [ H : @eq ?T _ _ |- _ ] =>
|
||||
match eval compute in T with
|
||||
| fmap _ _ => fail 1
|
||||
| _ => invert H
|
||||
end
|
||||
end.
|
||||
|
||||
Ltac maps_equal' := progress Frap.Map.M.maps_equal; autorewrite with core; simpl.
|
||||
|
||||
Ltac removeDups :=
|
||||
match goal with
|
||||
| [ |- context[constant ?ls] ] =>
|
||||
someMatch ls;
|
||||
erewrite (@removeDups_ok _ ls)
|
||||
by repeat (apply RdNil
|
||||
|| (apply RdNew; [ simpl; intuition (congruence || solve [ fancy_neq ]) | ])
|
||||
|| (apply RdDup; [ simpl; intuition (congruence || (repeat (maps_equal' || f_equal))) | ]))
|
||||
end.
|
||||
|
||||
Ltac doSubtract :=
|
||||
match goal with
|
||||
| [ |- context[constant ?ls \setminus constant ?ls0] ] =>
|
||||
erewrite (@doSubtract_ok _ ls ls0)
|
||||
by repeat (apply DsNil
|
||||
|| (apply DsKeep; [ simpl; intuition (congruence || solve [ fancy_neq ]) | ])
|
||||
|| (apply DsDrop; [ simpl; intuition (congruence || (repeat (maps_equal' || f_equal))) | ]))
|
||||
end.
|
||||
|
||||
Ltac simpl_maps :=
|
||||
repeat match goal with
|
||||
| [ |- context[add ?m ?k1 ?v $? ?k2] ] =>
|
||||
(rewrite (@lookup_add_ne _ _ m k1 k2 v) by (congruence || omega))
|
||||
|| (rewrite (@lookup_add_eq _ _ m k1 k2 v) by (congruence || omega))
|
||||
end.
|
||||
|
||||
Ltac simplify := repeat (unifyTails; pose proof I);
|
||||
repeat match goal with
|
||||
| [ H : True |- _ ] => clear H
|
||||
end;
|
||||
repeat progress (simpl in *; intros; try autorewrite with core in *; simpl_maps);
|
||||
repeat (normalize_set || doSubtract).
|
||||
Ltac propositional := intuition idtac.
|
||||
|
||||
Ltac linear_arithmetic := intros;
|
||||
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 := intuition 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);
|
||||
repeat match goal with
|
||||
| [ H : _ = left _ |- _ ] => clear H
|
||||
| [ H : _ = right _ |- _ ] => clear H
|
||||
end.
|
||||
|
||||
Global Opaque max min.
|
||||
|
||||
Infix "==n" := eq_nat_dec (no associativity, at level 50).
|
||||
Infix "<=?" := le_lt_dec.
|
||||
|
||||
Export Frap.Map.
|
||||
|
||||
Ltac maps_equal := Frap.Map.M.maps_equal; simplify.
|
||||
|
||||
Ltac first_order := firstorder idtac.
|
||||
|
||||
|
||||
(** * Model checking *)
|
||||
|
||||
Lemma eq_iff : forall P Q,
|
||||
P = Q
|
||||
-> (P <-> Q).
|
||||
Proof.
|
||||
equality.
|
||||
Qed.
|
||||
|
||||
Ltac sets0 := Sets.sets ltac:(simpl in *; intuition (subst; auto; try equality; try linear_arithmetic)).
|
||||
|
||||
Ltac sets := propositional;
|
||||
try match goal with
|
||||
| [ |- @eq (set _) _ _ ] =>
|
||||
let x := fresh "x" in
|
||||
apply sets_equal; intro x;
|
||||
repeat match goal with
|
||||
| [ H : @eq (set _) _ _ |- _ ] => apply (f_equal (fun f => f x)) in H;
|
||||
apply eq_iff in H
|
||||
end
|
||||
end; sets0;
|
||||
try match goal with
|
||||
| [ H : @eq (set ?T) _ _, x : ?T |- _ ] =>
|
||||
repeat match goal with
|
||||
| [ H : @eq (set T) _ _ |- _ ] => apply (f_equal (fun f => f x)) in H;
|
||||
apply eq_iff in H
|
||||
end;
|
||||
solve [ sets0 ]
|
||||
end.
|
||||
|
||||
Ltac model_check_invert1 :=
|
||||
match goal with
|
||||
| [ H : ?P |- _ ] =>
|
||||
match type of P with
|
||||
| Prop => invert H;
|
||||
repeat match goal with
|
||||
| [ H : existT _ ?x _ = existT _ ?x _ |- _ ] =>
|
||||
apply inj_pair2 in H; subst
|
||||
end; simplify
|
||||
end
|
||||
end.
|
||||
|
||||
Ltac model_check_invert := simplify; subst; repeat model_check_invert1.
|
||||
|
||||
Lemma oneStepClosure_solve : forall A (sys : trsys A) I I',
|
||||
oneStepClosure sys I I'
|
||||
-> I = I'
|
||||
-> oneStepClosure sys I I.
|
||||
Proof.
|
||||
equality.
|
||||
Qed.
|
||||
|
||||
Ltac singletoner := try (exfalso; solve [ sets ]);
|
||||
repeat match goal with
|
||||
(* | _ => apply singleton_in *)
|
||||
| [ |- _ ?S ] => idtac S; apply singleton_in
|
||||
| [ |- (_ \cup _) _ ] => apply singleton_in_other
|
||||
end.
|
||||
|
||||
Ltac closure :=
|
||||
repeat (apply oneStepClosure_empty
|
||||
|| (apply oneStepClosure_split; [ model_check_invert; try equality; solve [ singletoner ] | ])).
|
||||
|
||||
Ltac model_check_done :=
|
||||
apply MscDone; eapply oneStepClosure_solve; [ closure | simplify; solve [ sets ] ].
|
||||
|
||||
Ltac model_check_step0 :=
|
||||
eapply MscStep; [ closure | simplify ].
|
||||
|
||||
Ltac model_check_step :=
|
||||
match goal with
|
||||
| [ |- multiStepClosure _ ?inv1 _ _ ] =>
|
||||
model_check_step0;
|
||||
match goal with
|
||||
| [ |- multiStepClosure _ ?inv2 _ _ ] =>
|
||||
(assert (inv1 = inv2) by compare_sets; fail 3)
|
||||
|| idtac
|
||||
end
|
||||
end.
|
||||
|
||||
Ltac model_check_steps1 := model_check_step || model_check_done.
|
||||
Ltac model_check_steps := repeat model_check_steps1.
|
||||
|
||||
Ltac model_check_finish := simplify; propositional; subst; simplify; try equality; try linear_arithmetic.
|
||||
|
||||
Ltac model_check_infer :=
|
||||
apply multiStepClosure_ok; simplify; model_check_steps.
|
||||
|
||||
Ltac model_check_find_invariant :=
|
||||
simplify; eapply invariant_weaken; [ model_check_infer | ]; cbv beta in *.
|
||||
|
||||
Ltac model_check := model_check_find_invariant; model_check_finish.
|
||||
|
||||
Inductive ordering (n m : nat) :=
|
||||
| Lt (_ : n < m)
|
||||
| Eq (_ : n = m)
|
||||
| Gt (_ : n > m).
|
||||
|
||||
Local Hint Constructors ordering.
|
||||
Local Hint Extern 1 (_ < _) => omega.
|
||||
Local Hint Extern 1 (_ > _) => omega.
|
||||
|
||||
Theorem totally_ordered : forall n m, ordering n m.
|
||||
Proof.
|
||||
induction n; destruct m; simpl; eauto.
|
||||
destruct (IHn m); eauto.
|
||||
Qed.
|
||||
|
||||
Ltac total_ordering N M := destruct (totally_ordered N M).
|
||||
|
||||
Ltac inList x xs :=
|
||||
match xs with
|
||||
| (x, _) => true
|
||||
| (_, ?xs') => inList x xs'
|
||||
| _ => false
|
||||
end.
|
||||
|
||||
Ltac maybe_simplify_map m found kont :=
|
||||
match m with
|
||||
| @empty ?A ?B => kont (@empty A B)
|
||||
| ?m' $+ (?k, ?v) =>
|
||||
let iL := inList k found in
|
||||
match iL with
|
||||
| true => maybe_simplify_map m' found kont
|
||||
| false =>
|
||||
maybe_simplify_map m' (k, found) ltac:(fun m' => kont (m' $+ (k, v)))
|
||||
end
|
||||
end.
|
||||
|
||||
Ltac simplify_map' m found kont :=
|
||||
match m with
|
||||
| ?m' $+ (?k, ?v) =>
|
||||
let iL := inList k found in
|
||||
match iL with
|
||||
| true => maybe_simplify_map m' found kont
|
||||
| false =>
|
||||
simplify_map' m' (k, found) ltac:(fun m' => kont (m' $+ (k, v)))
|
||||
end
|
||||
end.
|
||||
|
||||
Ltac simplify_map :=
|
||||
match goal with
|
||||
| [ |- context[@add ?A ?B ?m ?k ?v] ] =>
|
||||
simplify_map' (m $+ (k, v)) tt ltac:(fun m' =>
|
||||
replace (@add A B m k v) with m' by maps_equal)
|
||||
end.
|
||||
|
||||
Require Import Classical.
|
||||
Ltac excluded_middle P := destruct (classic P).
|
||||
Module Export SN := SetNotations(FrapWithoutSets).
|
||||
|
|
373
FrapWithoutSets.v
Normal file
373
FrapWithoutSets.v
Normal file
|
@ -0,0 +1,373 @@
|
|||
Require Import Eqdep String Arith Omega Program Sets Relations Map Var Invariant Bool ModelCheck.
|
||||
Export String Arith Sets Relations Map Var Invariant Bool ModelCheck.
|
||||
Require Import List.
|
||||
Export List ListNotations.
|
||||
Open Scope string_scope.
|
||||
Open Scope list_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 same_structure x y :=
|
||||
match x with
|
||||
| ?f ?a1 ?b1 ?c1 ?d1 =>
|
||||
match y with
|
||||
| f ?a2 ?b2 ?c2 ?d2 => same_structure a1 a2; same_structure b1 b2; same_structure c1 c2; same_structure d1 d2
|
||||
| _ => fail 2
|
||||
end
|
||||
| ?f ?a1 ?b1 ?c1 =>
|
||||
match y with
|
||||
| f ?a2 ?b2 ?c2 => same_structure a1 a2; same_structure b1 b2; same_structure c1 c2
|
||||
| _ => fail 2
|
||||
end
|
||||
| ?f ?a1 ?b1 =>
|
||||
match y with
|
||||
| f ?a2 ?b2 => same_structure a1 a2; same_structure b1 b2
|
||||
| _ => fail 2
|
||||
end
|
||||
| ?f ?a1 =>
|
||||
match y with
|
||||
| f ?a2 => same_structure a1 a2
|
||||
| _ => fail 2
|
||||
end
|
||||
| _ =>
|
||||
match y with
|
||||
| ?f ?a1 ?b1 ?c1 ?d1 =>
|
||||
match x with
|
||||
| f ?a2 ?b2 ?c2 ?d2 => same_structure a1 a2; same_structure b1 b2; same_structure c1 c2; same_structure d1 d2
|
||||
| _ => fail 2
|
||||
end
|
||||
| ?f ?a1 ?b1 ?c1 =>
|
||||
match x with
|
||||
| f ?a2 ?b2 ?c2 => same_structure a1 a2; same_structure b1 b2; same_structure c1 c2
|
||||
| _ => fail 2
|
||||
end
|
||||
| ?f ?a1 ?b1 =>
|
||||
match x with
|
||||
| f ?a2 ?b2 => same_structure a1 a2; same_structure b1 b2
|
||||
| _ => fail 2
|
||||
end
|
||||
| ?f ?a1 =>
|
||||
match x with
|
||||
| f ?a2 => same_structure a1 a2
|
||||
| _ => fail 2
|
||||
end
|
||||
| _ => idtac
|
||||
end
|
||||
end.
|
||||
|
||||
Ltac instantiate_obvious1 H :=
|
||||
match type of H with
|
||||
| _ ++ _ = _ ++ _ -> _ => fail 1
|
||||
| ?x = ?y -> _ =>
|
||||
(same_structure x y; specialize (H eq_refl))
|
||||
|| (has_evar (x, y); fail 3)
|
||||
| JMeq.JMeq ?x ?y -> _ =>
|
||||
(same_structure x y; specialize (H JMeq.JMeq_refl))
|
||||
|| (has_evar (x, y); fail 3)
|
||||
| forall x : ?T, _ =>
|
||||
match type of T with
|
||||
| Prop => fail 1
|
||||
| _ =>
|
||||
let x' := fresh x in
|
||||
evar (x' : T);
|
||||
let x'' := eval unfold x' in x' in specialize (H x''); clear x';
|
||||
instantiate_obvious1 H
|
||||
end
|
||||
end.
|
||||
|
||||
Ltac instantiate_obvious H :=
|
||||
match type of H with
|
||||
| context[@eq string _ _] => idtac
|
||||
| _ => repeat instantiate_obvious1 H
|
||||
end.
|
||||
|
||||
Ltac instantiate_obviouses :=
|
||||
repeat match goal with
|
||||
| [ H : _ |- _ ] => instantiate_obvious H
|
||||
end.
|
||||
|
||||
Ltac induct e := (inductN e || dependent induction e); instantiate_obviouses.
|
||||
|
||||
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 maps_neq :=
|
||||
match goal with
|
||||
| [ H : ?m1 = ?m2 |- _ ] =>
|
||||
let rec recur E :=
|
||||
match E with
|
||||
| ?E' $+ (?k, _) =>
|
||||
(apply (f_equal (fun m => m $? k)) in H; simpl in *; autorewrite with core in *; simpl in *; congruence)
|
||||
|| recur E'
|
||||
end in
|
||||
recur m1 || recur m2
|
||||
end.
|
||||
|
||||
Ltac fancy_neq :=
|
||||
repeat match goal with
|
||||
| _ => maps_neq
|
||||
| [ H : @eq (nat -> _) _ _ |- _ ] => apply (f_equal (fun f => f 0)) in H
|
||||
| [ H : @eq ?T _ _ |- _ ] =>
|
||||
match eval compute in T with
|
||||
| fmap _ _ => fail 1
|
||||
| _ => invert H
|
||||
end
|
||||
end.
|
||||
|
||||
Ltac maps_equal' := progress Frap.Map.M.maps_equal; autorewrite with core; simpl.
|
||||
|
||||
Ltac removeDups :=
|
||||
match goal with
|
||||
| [ |- context[constant ?ls] ] =>
|
||||
someMatch ls;
|
||||
erewrite (@removeDups_ok _ ls)
|
||||
by repeat (apply RdNil
|
||||
|| (apply RdNew; [ simpl; intuition (congruence || solve [ fancy_neq ]) | ])
|
||||
|| (apply RdDup; [ simpl; intuition (congruence || (repeat (maps_equal' || f_equal))) | ]))
|
||||
end.
|
||||
|
||||
Ltac doSubtract :=
|
||||
match goal with
|
||||
| [ |- context[constant ?ls \setminus constant ?ls0] ] =>
|
||||
erewrite (@doSubtract_ok _ ls ls0)
|
||||
by repeat (apply DsNil
|
||||
|| (apply DsKeep; [ simpl; intuition (congruence || solve [ fancy_neq ]) | ])
|
||||
|| (apply DsDrop; [ simpl; intuition (congruence || (repeat (maps_equal' || f_equal))) | ]))
|
||||
end.
|
||||
|
||||
Ltac simpl_maps :=
|
||||
repeat match goal with
|
||||
| [ |- context[add ?m ?k1 ?v $? ?k2] ] =>
|
||||
(rewrite (@lookup_add_ne _ _ m k1 k2 v) by (congruence || omega))
|
||||
|| (rewrite (@lookup_add_eq _ _ m k1 k2 v) by (congruence || omega))
|
||||
end.
|
||||
|
||||
Ltac simplify := repeat (unifyTails; pose proof I);
|
||||
repeat match goal with
|
||||
| [ H : True |- _ ] => clear H
|
||||
end;
|
||||
repeat progress (simpl in *; intros; try autorewrite with core in *; simpl_maps);
|
||||
repeat (normalize_set || doSubtract).
|
||||
Ltac propositional := intuition idtac.
|
||||
|
||||
Ltac linear_arithmetic := intros;
|
||||
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 := intuition 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);
|
||||
repeat match goal with
|
||||
| [ H : _ = left _ |- _ ] => clear H
|
||||
| [ H : _ = right _ |- _ ] => clear H
|
||||
end.
|
||||
|
||||
Global Opaque max min.
|
||||
|
||||
Infix "==n" := eq_nat_dec (no associativity, at level 50).
|
||||
Infix "<=?" := le_lt_dec.
|
||||
|
||||
Export Frap.Map.
|
||||
|
||||
Ltac maps_equal := Frap.Map.M.maps_equal; simplify.
|
||||
|
||||
Ltac first_order := firstorder idtac.
|
||||
|
||||
|
||||
(** * Model checking *)
|
||||
|
||||
Lemma eq_iff : forall P Q,
|
||||
P = Q
|
||||
-> (P <-> Q).
|
||||
Proof.
|
||||
equality.
|
||||
Qed.
|
||||
|
||||
Ltac sets0 := Sets.sets ltac:(simpl in *; intuition (subst; auto; try equality; try linear_arithmetic)).
|
||||
|
||||
Ltac sets := propositional;
|
||||
try match goal with
|
||||
| [ |- @eq (set _) _ _ ] =>
|
||||
let x := fresh "x" in
|
||||
apply sets_equal; intro x;
|
||||
repeat match goal with
|
||||
| [ H : @eq (set _) _ _ |- _ ] => apply (f_equal (fun f => f x)) in H;
|
||||
apply eq_iff in H
|
||||
end
|
||||
end; sets0;
|
||||
try match goal with
|
||||
| [ H : @eq (set ?T) _ _, x : ?T |- _ ] =>
|
||||
repeat match goal with
|
||||
| [ H : @eq (set T) _ _ |- _ ] => apply (f_equal (fun f => f x)) in H;
|
||||
apply eq_iff in H
|
||||
end;
|
||||
solve [ sets0 ]
|
||||
end.
|
||||
|
||||
Ltac model_check_invert1 :=
|
||||
match goal with
|
||||
| [ H : ?P |- _ ] =>
|
||||
match type of P with
|
||||
| Prop => invert H;
|
||||
repeat match goal with
|
||||
| [ H : existT _ ?x _ = existT _ ?x _ |- _ ] =>
|
||||
apply inj_pair2 in H; subst
|
||||
end; simplify
|
||||
end
|
||||
end.
|
||||
|
||||
Ltac model_check_invert := simplify; subst; repeat model_check_invert1.
|
||||
|
||||
Lemma oneStepClosure_solve : forall A (sys : trsys A) I I',
|
||||
oneStepClosure sys I I'
|
||||
-> I = I'
|
||||
-> oneStepClosure sys I I.
|
||||
Proof.
|
||||
equality.
|
||||
Qed.
|
||||
|
||||
Ltac singletoner := try (exfalso; solve [ sets ]);
|
||||
repeat match goal with
|
||||
(* | _ => apply singleton_in *)
|
||||
| [ |- _ ?S ] => idtac S; apply singleton_in
|
||||
| [ |- (_ \cup _) _ ] => apply singleton_in_other
|
||||
end.
|
||||
|
||||
Ltac closure :=
|
||||
repeat (apply oneStepClosure_empty
|
||||
|| (apply oneStepClosure_split; [ model_check_invert; try equality; solve [ singletoner ] | ])).
|
||||
|
||||
Ltac model_check_done :=
|
||||
apply MscDone; eapply oneStepClosure_solve; [ closure | simplify; solve [ sets ] ].
|
||||
|
||||
Ltac model_check_step0 :=
|
||||
eapply MscStep; [ closure | simplify ].
|
||||
|
||||
Ltac model_check_step :=
|
||||
match goal with
|
||||
| [ |- multiStepClosure _ ?inv1 _ _ ] =>
|
||||
model_check_step0;
|
||||
match goal with
|
||||
| [ |- multiStepClosure _ ?inv2 _ _ ] =>
|
||||
(assert (inv1 = inv2) by compare_sets; fail 3)
|
||||
|| idtac
|
||||
end
|
||||
end.
|
||||
|
||||
Ltac model_check_steps1 := model_check_step || model_check_done.
|
||||
Ltac model_check_steps := repeat model_check_steps1.
|
||||
|
||||
Ltac model_check_finish := simplify; propositional; subst; simplify; try equality; try linear_arithmetic.
|
||||
|
||||
Ltac model_check_infer :=
|
||||
apply multiStepClosure_ok; simplify; model_check_steps.
|
||||
|
||||
Ltac model_check_find_invariant :=
|
||||
simplify; eapply invariant_weaken; [ model_check_infer | ]; cbv beta in *.
|
||||
|
||||
Ltac model_check := model_check_find_invariant; model_check_finish.
|
||||
|
||||
Inductive ordering (n m : nat) :=
|
||||
| Lt (_ : n < m)
|
||||
| Eq (_ : n = m)
|
||||
| Gt (_ : n > m).
|
||||
|
||||
Local Hint Constructors ordering.
|
||||
Local Hint Extern 1 (_ < _) => omega.
|
||||
Local Hint Extern 1 (_ > _) => omega.
|
||||
|
||||
Theorem totally_ordered : forall n m, ordering n m.
|
||||
Proof.
|
||||
induction n; destruct m; simpl; eauto.
|
||||
destruct (IHn m); eauto.
|
||||
Qed.
|
||||
|
||||
Ltac total_ordering N M := destruct (totally_ordered N M).
|
||||
|
||||
Ltac inList x xs :=
|
||||
match xs with
|
||||
| (x, _) => true
|
||||
| (_, ?xs') => inList x xs'
|
||||
| _ => false
|
||||
end.
|
||||
|
||||
Ltac maybe_simplify_map m found kont :=
|
||||
match m with
|
||||
| @empty ?A ?B => kont (@empty A B)
|
||||
| ?m' $+ (?k, ?v) =>
|
||||
let iL := inList k found in
|
||||
match iL with
|
||||
| true => maybe_simplify_map m' found kont
|
||||
| false =>
|
||||
maybe_simplify_map m' (k, found) ltac:(fun m' => kont (m' $+ (k, v)))
|
||||
end
|
||||
end.
|
||||
|
||||
Ltac simplify_map' m found kont :=
|
||||
match m with
|
||||
| ?m' $+ (?k, ?v) =>
|
||||
let iL := inList k found in
|
||||
match iL with
|
||||
| true => maybe_simplify_map m' found kont
|
||||
| false =>
|
||||
simplify_map' m' (k, found) ltac:(fun m' => kont (m' $+ (k, v)))
|
||||
end
|
||||
end.
|
||||
|
||||
Ltac simplify_map :=
|
||||
match goal with
|
||||
| [ |- context[@add ?A ?B ?m ?k ?v] ] =>
|
||||
simplify_map' (m $+ (k, v)) tt ltac:(fun m' =>
|
||||
replace (@add A B m k v) with m' by maps_equal)
|
||||
end.
|
||||
|
||||
Require Import Classical.
|
||||
Ltac excluded_middle P := destruct (classic P).
|
12
Map.v
12
Map.v
|
@ -64,7 +64,7 @@ Module Type S.
|
|||
-> (m1 $++ m2) $? k = m2 $? k.
|
||||
|
||||
Axiom join_comm : forall A B (m1 m2 : fmap A B),
|
||||
dom m1 \cap dom m2 = {}
|
||||
dom m1 \cap dom m2 = constant nil
|
||||
-> m1 $++ m2 = m2 $++ m1.
|
||||
|
||||
Axiom join_assoc : forall A B (m1 m2 m3 : fmap A B),
|
||||
|
@ -116,10 +116,10 @@ Module Type S.
|
|||
|
||||
Axiom empty_includes : forall A B (m : fmap A B), empty A B $<= m.
|
||||
|
||||
Axiom dom_empty : forall A B, dom (empty A B) = {}.
|
||||
Axiom dom_empty : forall A B, dom (empty A B) = constant nil.
|
||||
|
||||
Axiom dom_add : forall A B (m : fmap A B) (k : A) (v : B),
|
||||
dom (add m k v) = {k} \cup dom m.
|
||||
dom (add m k v) = constant (k :: nil) \cup dom m.
|
||||
|
||||
Axiom lookup_restrict_true : forall A B (P : A -> Prop) (m : fmap A B) k,
|
||||
P k
|
||||
|
@ -390,7 +390,7 @@ Module M : S.
|
|||
Qed.
|
||||
|
||||
Theorem join_comm : forall A B (m1 m2 : fmap A B),
|
||||
dom m1 \cap dom m2 = {}
|
||||
dom m1 \cap dom m2 = constant nil
|
||||
-> join m1 m2 = join m2 m1.
|
||||
Proof.
|
||||
intros; apply fmap_ext; unfold join, lookup; intros.
|
||||
|
@ -508,13 +508,13 @@ Module M : S.
|
|||
unfold includes, empty; intuition congruence.
|
||||
Qed.
|
||||
|
||||
Theorem dom_empty : forall A B, dom (empty (A := A) B) = {}.
|
||||
Theorem dom_empty : forall A B, dom (empty (A := A) B) = constant nil.
|
||||
Proof.
|
||||
unfold dom, empty; intros; sets idtac.
|
||||
Qed.
|
||||
|
||||
Theorem dom_add : forall A B (m : fmap A B) (k : A) (v : B),
|
||||
dom (add m k v) = {k} \cup dom m.
|
||||
dom (add m k v) = constant (k :: nil) \cup dom m.
|
||||
Proof.
|
||||
unfold dom, add; simpl; intros.
|
||||
sets ltac:(simpl in *; try match goal with
|
||||
|
|
|
@ -10,11 +10,11 @@ Set Asymmetric Patterns.
|
|||
|
||||
(** * First, an unexplained tactic that will come in handy.... *)
|
||||
|
||||
Ltac invert H := (Frap.invert H || (inversion H; clear H));
|
||||
repeat match goal with
|
||||
| [ x : _ |- _ ] => subst x
|
||||
| [ H : existT _ _ _ = existT _ _ _ |- _ ] => apply inj_pair2 in H; try subst
|
||||
end.
|
||||
Ltac invert H := (FrapWithoutSets.invert H || (inversion H; clear H));
|
||||
repeat match goal with
|
||||
| [ x : _ |- _ ] => subst x
|
||||
| [ H : existT _ _ _ = existT _ _ _ |- _ ] => apply inj_pair2 in H; try subst
|
||||
end.
|
||||
|
||||
|
||||
(** * A process algebra: syntax and semantics *)
|
||||
|
|
|
@ -75,7 +75,7 @@ Qed.
|
|||
Theorem oneStepClosure_split : forall state (sys : trsys state) st sts (inv1 inv2 : state -> Prop),
|
||||
(forall st', sys.(Step) st st' -> inv1 st')
|
||||
-> oneStepClosure sys (constant sts) inv2
|
||||
-> oneStepClosure sys (constant (st :: sts)) ({st} \cup inv1 \cup inv2).
|
||||
-> oneStepClosure sys (constant (st :: sts)) (constant (st :: nil) \cup inv1 \cup inv2).
|
||||
Proof.
|
||||
unfold oneStepClosure, oneStepClosure_current, oneStepClosure_new; intuition.
|
||||
|
||||
|
@ -89,7 +89,7 @@ Proof.
|
|||
Qed.
|
||||
|
||||
Theorem singleton_in : forall {A} (x : A) rest,
|
||||
({x} \cup rest) x.
|
||||
(constant (x :: nil) \cup rest) x.
|
||||
Proof.
|
||||
unfold union; simpl; auto.
|
||||
Qed.
|
||||
|
|
|
@ -28,3 +28,7 @@ The main narrative, also present in the book PDF, presents standard program-proo
|
|||
* Chapter 15: `SharedMemory.v`
|
||||
* Chapter 16: `ConcurrentSeparationLogic.v`
|
||||
* Chapter 17: `MessagesAndRefinement.v`
|
||||
|
||||
There are also two supplementary files that are independent of the main narrative, for introducing programming with dependent types, a distinctive Coq feature that we neither use nor recommend for the problem sets, but which many students find interesting (and useful in other contexts).
|
||||
* `SubsetTypes.v`: a first introduction to dependent types by attaching predicates to normal types (used after `CompilerCorrectness.v` in the last course offering)
|
||||
* One more coming soon
|
||||
|
|
16
Sets.v
16
Sets.v
|
@ -35,8 +35,6 @@ Section set.
|
|||
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).
|
||||
|
@ -45,6 +43,14 @@ Infix "\subseteq" := subseteq (at level 70).
|
|||
Infix "\subset" := subset (at level 70).
|
||||
Notation "[ x | P ]" := (scomp (fun x => P)).
|
||||
|
||||
Module Type EMPTY.
|
||||
End EMPTY.
|
||||
Module SetNotations(M : EMPTY).
|
||||
Notation "{ }" := (constant nil).
|
||||
Notation "{ x1 , .. , xN }" := (constant (cons x1 (.. (cons xN nil) ..))).
|
||||
End SetNotations.
|
||||
|
||||
|
||||
Ltac sets' tac :=
|
||||
unfold In, constant, universe, check, union, intersection, minus, complement, subseteq, subset, scomp in *;
|
||||
tauto || intuition tac.
|
||||
|
@ -288,7 +294,7 @@ Section setexpr.
|
|||
match e with
|
||||
| Literal vs =>
|
||||
match env with
|
||||
| [] => {}
|
||||
| [] => constant []
|
||||
| x :: _ => constant (map (nth_default x env) vs)
|
||||
end
|
||||
| Constant s => s
|
||||
|
@ -339,7 +345,7 @@ Section setexpr.
|
|||
|
||||
Definition interp_normal_form (env : list A) (nf : normal_form) : set A :=
|
||||
let cs := match env with
|
||||
| [] => {}
|
||||
| [] => constant []
|
||||
| x :: _ => constant (map (nth_default x env) nf.(Elements))
|
||||
end in
|
||||
match nf.(Other) with
|
||||
|
@ -557,7 +563,7 @@ Ltac quote E env k :=
|
|||
quote' E2 env' ltac:(fun e2 env'' =>
|
||||
k (Union e1 e2) env''))
|
||||
| _ =>
|
||||
(let pf := constr:(eq_refl : E = {}) in
|
||||
(let pf := constr:(eq_refl : E = constant []) in
|
||||
k (Literal A []) env)
|
||||
|| k (Constant E) env
|
||||
end in
|
||||
|
|
633
SubsetTypes.v
Normal file
633
SubsetTypes.v
Normal file
|
@ -0,0 +1,633 @@
|
|||
(** Formal Reasoning About Programs <http://adam.chlipala.net/frap/>
|
||||
* Supplementary Coq material: subset types
|
||||
* Author: Adam Chlipala
|
||||
* License: https://creativecommons.org/licenses/by-nc-nd/4.0/
|
||||
* Much of the material comes from CPDT <http://adam.chlipala.net/cpdt/> by the same author. *)
|
||||
|
||||
Require Import FrapWithoutSets.
|
||||
(* We import a pared-down version of the book library, to avoid notations that
|
||||
* clash with some we want to use here. *)
|
||||
|
||||
Set Implicit Arguments.
|
||||
Set Asymmetric Patterns.
|
||||
(* Compatibility flag that affects pattern matching for fancy types *)
|
||||
|
||||
|
||||
(* So far, we have seen many examples of what we might call "classical program
|
||||
* verification." We write programs, write their specifications, and then prove
|
||||
* that the programs satisfy their specifications. The programs that we have
|
||||
* written in Coq have been normal functional programs that we could just as
|
||||
* well have written in Haskell or ML. In this lecture, we start investigating
|
||||
* uses of _dependent types_ to integrate programming, specification, and
|
||||
* proving into a single phase. The techniques we will learn make it possible
|
||||
* to reduce the cost of program verification dramatically. *)
|
||||
|
||||
|
||||
(** * Introducing Subset Types *)
|
||||
|
||||
(** Let us consider several ways of implementing the natural-number-predecessor
|
||||
* function. We start by displaying the definition from the standard library: *)
|
||||
|
||||
Compute pred.
|
||||
|
||||
(* We can use a new command, [Extraction], to produce an OCaml version of this
|
||||
* function. *)
|
||||
|
||||
Extraction pred.
|
||||
|
||||
(* Returning 0 as the predecessor of 0 can come across as somewhat of a hack.
|
||||
* In some situations, we might like to be sure that we never try to take the
|
||||
* predecessor of 0. We can enforce this by giving [pred] a stronger, dependent
|
||||
* type. *)
|
||||
|
||||
Lemma zgtz : 0 > 0 -> False.
|
||||
Proof.
|
||||
linear_arithmetic.
|
||||
Qed.
|
||||
|
||||
Definition pred_strong1 (n : nat) : n > 0 -> nat :=
|
||||
match n with
|
||||
| O => fun pf : 0 > 0 => match zgtz pf with end
|
||||
| S n' => fun _ => n'
|
||||
end.
|
||||
|
||||
(* We expand the type of [pred] to include a _proof_ that its argument [n] is
|
||||
* greater than 0. When [n] is 0, we use the proof to derive a contradiction,
|
||||
* which we can use to build a value of any type via a vacuous pattern match.
|
||||
* When [n] is a successor, we have no need for the proof and just return the
|
||||
* answer. The proof argument can be said to have a _dependent_ type, because
|
||||
* its type depends on the _value_ of the argument [n].
|
||||
*
|
||||
* Coq's [Compute] command can execute particular invocations of [pred_strong1]
|
||||
* just as easily as it can execute more traditional functional programs. *)
|
||||
|
||||
Theorem two_gt0 : 2 > 0.
|
||||
Proof.
|
||||
linear_arithmetic.
|
||||
Qed.
|
||||
|
||||
Compute pred_strong1 two_gt0.
|
||||
|
||||
(* One aspect in particular of the definition of [pred_strong1] may be
|
||||
* surprising. We took advantage of [Definition]'s syntactic sugar for defining
|
||||
* function arguments in the case of [n], but we bound the proofs later with
|
||||
* explicit [fun] expressions. Let us see what happens if we write this
|
||||
* function in the way that at first seems most natural. *)
|
||||
|
||||
Fail Definition pred_strong1' (n : nat) (pf : n > 0) : nat :=
|
||||
match n with
|
||||
| O => match zgtz pf with end
|
||||
| S n' => n'
|
||||
end.
|
||||
|
||||
(* The term [zgtz pf] fails to type-check. Somehow the type checker has failed
|
||||
* to take into account information that follows from which [match] branch that
|
||||
* term appears in. The problem is that, by default, [match] does not let us
|
||||
* use such implied information. To get refined typing, we must always rely on
|
||||
* [match] annotations, either written explicitly or inferred.
|
||||
*
|
||||
* In this case, we must use a [return] annotation to declare the relationship
|
||||
* between the _value_ of the [match] discriminee and the _type_ of the result.
|
||||
* There is no annotation that lets us declare a relationship between the
|
||||
* discriminee and the type of a variable that is already in scope; hence, we
|
||||
* delay the binding of [pf], so that we can use the [return] annotation to
|
||||
* express the needed relationship.
|
||||
*
|
||||
* We are lucky that Coq's heuristics infer the [return] clause (specifically,
|
||||
* [return n > 0 -> nat]) for us in the definition of [pred_strong1], leading to
|
||||
* the following elaborated code: *)
|
||||
|
||||
Definition pred_strong1' (n : nat) : n > 0 -> nat :=
|
||||
match n return n > 0 -> nat with
|
||||
| O => fun pf : 0 > 0 => match zgtz pf with end
|
||||
| S n' => fun _ => n'
|
||||
end.
|
||||
|
||||
(* By making explicit the functional relationship between value [n] and the
|
||||
* result type of the [match], we guide Coq toward proper type checking. The
|
||||
* clause for this example follows by simple copying of the original annotation
|
||||
* on the definition. In general, however, the [match] annotation inference
|
||||
* problem is undecidable. The known undecidable problem of
|
||||
* _higher-order unification_ reduces to the [match] type inference problem.
|
||||
* Over time, Coq is enhanced with more and more heuristics to get around this
|
||||
* problem, but there must always exist [match]es whose types Coq cannot infer
|
||||
* without annotations.
|
||||
*
|
||||
* Let us now take a look at the OCaml code Coq generates for [pred_strong1]. *)
|
||||
|
||||
Extraction pred_strong1.
|
||||
|
||||
(* The proof argument has disappeared! We get exactly the OCaml code we would
|
||||
* have written manually. This is our first demonstration of the main
|
||||
* technically interesting feature of Coq program extraction: proofs are erased
|
||||
* systematically.
|
||||
*
|
||||
* We can reimplement our dependently typed [pred] based on _subset types_,
|
||||
* defined in the standard library with the type family %[sig]. *)
|
||||
|
||||
Print sig.
|
||||
|
||||
(* We rewrite [pred_strong1], using some syntactic sugar for subset types, after
|
||||
* we deactivate some clashing notations for set literals. *)
|
||||
|
||||
Locate "{ _ : _ | _ }".
|
||||
|
||||
Definition pred_strong2 (s : {n : nat | n > 0} ) : nat :=
|
||||
match s with
|
||||
| exist O pf => match zgtz pf with end
|
||||
| exist (S n') _ => n'
|
||||
end.
|
||||
|
||||
(* To build a value of a subset type, we use the [exist] constructor, and the
|
||||
* details of how to do that follow from the output of our earlier [Print sig]
|
||||
* command, where we elided the extra information that parameter [A] is
|
||||
* implicit. We need an extra [_] here and not in the definition of
|
||||
* [pred_strong2] because _parameters_ of inductive types (like the predicate
|
||||
* [P] for [sig]) are not mentioned in pattern matching, but _are_ mentioned in
|
||||
* construction of terms (if they are not marked as implicit arguments).
|
||||
* (Actually, this behavior changed between Coq versions 8.4 and 8.5, hence the
|
||||
* near at the top of the file to revert to the old behavior.) *)
|
||||
|
||||
Compute pred_strong2 (exist _ 2 two_gt0).
|
||||
|
||||
Extraction pred_strong2.
|
||||
|
||||
(* We arrive at the same OCaml code as was extracted from [pred_strong1], which
|
||||
* may seem surprising at first. The reason is that a value of [sig] is a pair
|
||||
* of two pieces, a value and a proof about it. Extraction erases the proof,
|
||||
* which reduces the constructor [exist] of [sig] to taking just a single
|
||||
* argument. An optimization eliminates uses of datatypes with single
|
||||
* constructors taking single arguments, and we arrive back where we started.
|
||||
*
|
||||
* We can continue on in the process of refining [pred]'s type. Let us change
|
||||
* its result type to capture that the output is really the predecessor of the
|
||||
* input. *)
|
||||
|
||||
Definition pred_strong3 (s : {n : nat | n > 0}) : {m : nat | proj1_sig s = S m} :=
|
||||
match s return {m : nat | proj1_sig s = S m} with
|
||||
| exist 0 pf => match zgtz pf with end
|
||||
| exist (S n') pf => exist _ n' (eq_refl _)
|
||||
end.
|
||||
|
||||
Compute pred_strong3 (exist _ 2 two_gt0).
|
||||
|
||||
(* A value in a subset type can be thought of as a _dependent pair_ (or
|
||||
* _sigma type_ of a base value and a proof about it. The function [proj1_sig]
|
||||
* extracts the first component of the pair. It turns out that we need to
|
||||
* include an explicit [return] clause here, since Coq's heuristics are not
|
||||
* smart enough to propagate the result type that we wrote earlier.
|
||||
*
|
||||
* By now, the reader is probably ready to believe that the new [pred_strong]
|
||||
* leads to the same OCaml code as we have seen several times so far, and Coq
|
||||
* does not disappoint. *)
|
||||
|
||||
Extraction pred_strong3.
|
||||
|
||||
(* We have managed to reach a type that is, in a formal sense, the most
|
||||
* expressive possible for [pred]. Any other implementation of the same type
|
||||
* must have the same input-output behavior. However, there is still room for
|
||||
* improvement in making this kind of code easier to write. Here is a version
|
||||
* that takes advantage of tactic-based theorem proving. We switch back to
|
||||
* passing a separate proof argument instead of using a subset type for the
|
||||
* function's input, because this leads to cleaner code. ([False_rec] is a
|
||||
* library function that can be used to produce a value in any type given a
|
||||
* proof of [False]. It's defined in terms of the vacuous pattern match we saw
|
||||
* earlier.) *)
|
||||
|
||||
Definition pred_strong4 : forall (n : nat), n > 0 -> {m : nat | n = S m}.
|
||||
refine (fun n =>
|
||||
match n with
|
||||
| O => fun _ => False_rec _ _
|
||||
| S n' => fun _ => exist _ n' _
|
||||
end).
|
||||
|
||||
(* We build [pred_strong4] using tactic-based proving, beginning with a
|
||||
* [Definition] command that ends in a period before a definition is given.
|
||||
* Such a command enters the interactive proving mode, with the type given for
|
||||
* the new identifier as our proof goal.
|
||||
*
|
||||
* We do most of the work with the [refine] tactic, to which we pass a partial
|
||||
* "proof" of the type we are trying to prove. There may be some pieces left
|
||||
* to fill in, indicated by underscores. Any underscore that Coq cannot
|
||||
* reconstruct with type inference is added as a proof subgoal. In this case,
|
||||
* we have two subgoals.
|
||||
*
|
||||
* We can see that the first subgoal comes from the second underscore passed
|
||||
* to [False_rec], and the second subgoal comes from the second underscore
|
||||
* passed to [exist]. In the first case, we see that, though we bound the
|
||||
* proof variable with an underscore, it is still available in our proof
|
||||
* context. It is hard to refer to underscore-named variables in manual
|
||||
* proofs, but automation makes short work of them. Both subgoals are easy to
|
||||
* discharge that way, so let us back up and ask to prove all subgoals
|
||||
* automatically. *)
|
||||
|
||||
Undo.
|
||||
refine (fun n =>
|
||||
match n with
|
||||
| O => fun _ => False_rec _ _
|
||||
| S n' => fun _ => exist _ n' _
|
||||
end); equality || linear_arithmetic.
|
||||
Defined.
|
||||
|
||||
(* We end the "proof" with [Defined] instead of [Qed], so that the definition we
|
||||
* constructed remains visible. This contrasts to the case of ending a proof
|
||||
* with [Qed], where the details of the proof are hidden afterward. (More
|
||||
* formally, [Defined] marks an identifier as _transparent_, allowing it to be
|
||||
* unfolded; while [Qed] marks an identifier as _opaque_, preventing unfolding.)
|
||||
* Let us see what our proof script constructed. *)
|
||||
|
||||
Print pred_strong4.
|
||||
|
||||
(* We see the code we entered, with some (pretty long!) proofs filled in. *)
|
||||
|
||||
Compute pred_strong4 two_gt0.
|
||||
|
||||
(* We are almost done with the ideal implementation of dependent predecessor.
|
||||
* We can use Coq's syntax extension facility to arrive at code with almost no
|
||||
* complexity beyond a Haskell or ML program with a complete specification in a
|
||||
* comment. In this book, we will not dwell on the details of syntax
|
||||
* extensions; the Coq manual gives a straightforward introduction to them. *)
|
||||
|
||||
Notation "!" := (False_rec _ _).
|
||||
Notation "[ e ]" := (exist _ e _).
|
||||
|
||||
Definition pred_strong5 : forall (n : nat), n > 0 -> {m : nat | n = S m}.
|
||||
refine (fun n =>
|
||||
match n with
|
||||
| O => fun _ => !
|
||||
| S n' => fun _ => [n']
|
||||
end); equality || linear_arithmetic.
|
||||
Defined.
|
||||
|
||||
(* By default, notations are also used in pretty-printing terms, including
|
||||
* results of evaluation. *)
|
||||
|
||||
Compute pred_strong5 two_gt0.
|
||||
|
||||
|
||||
(** * Decidable Proposition Types *)
|
||||
|
||||
(* There is another type in the standard library that captures the idea of
|
||||
* program values that indicate which of two propositions is true. *)
|
||||
|
||||
Print sumbool.
|
||||
|
||||
(* Here, the constructors of [sumbool] have types written in terms of a
|
||||
* registered notation for [sumbool], such that the result type of each
|
||||
* constructor desugars to [sumbool A B]. We can define some notations of our
|
||||
* own to make working with [sumbool] more convenient. *)
|
||||
|
||||
Notation "'Yes'" := (left _ _).
|
||||
Notation "'No'" := (right _ _).
|
||||
Notation "'Reduce' x" := (if x then Yes else No) (at level 50).
|
||||
|
||||
(* The [Reduce] notation is notable because it demonstrates how [if] is
|
||||
* overloaded in Coq. The [if] form actually works when the test expression has
|
||||
* any two-constructor inductive type. Moreover, in the [then] and [else]
|
||||
* branches, the appropriate constructor arguments are bound. This is important
|
||||
* when working with [sumbool]s, when we want to have the proof stored in the
|
||||
* test expression available when proving the proof obligations generated in the
|
||||
* appropriate branch.
|
||||
*
|
||||
* Now we can write [eq_nat_dec], which compares two natural numbers, returning
|
||||
* either a proof of their equality or a proof of their inequality. *)
|
||||
|
||||
Definition eq_nat_dec : forall n m : nat, {n = m} + {n <> m}.
|
||||
refine (fix f (n m : nat) : {n = m} + {n <> m} :=
|
||||
match n, m with
|
||||
| O, O => Yes
|
||||
| S n', S m' => Reduce (f n' m')
|
||||
| _, _ => No
|
||||
end); equality.
|
||||
Defined.
|
||||
|
||||
Compute eq_nat_dec 2 2.
|
||||
Compute eq_nat_dec 2 3.
|
||||
|
||||
(* Note that the [Yes] and [No] notations are hiding proofs establishing the
|
||||
* correctness of the outputs.
|
||||
*
|
||||
* Our definition extracts to reasonable OCaml code. *)
|
||||
|
||||
Extraction eq_nat_dec.
|
||||
|
||||
(* Proving this kind of decidable equality result is so common that Coq comes
|
||||
* with a tactic for automating it. *)
|
||||
|
||||
Definition eq_nat_dec' (n m : nat) : {n = m} + {n <> m}.
|
||||
decide equality.
|
||||
Defined.
|
||||
|
||||
(* Curious readers can verify that the [decide equality] version extracts to the
|
||||
* same OCaml code as our more manual version does. That OCaml code had one
|
||||
* undesirable property, which is that it uses [Left] and [Right] constructors
|
||||
* instead of the Boolean values built into OCaml. We can fix this, by using
|
||||
* Coq's facility for mapping Coq inductive types to OCaml variant types. *)
|
||||
|
||||
Extract Inductive sumbool => "bool" ["true" "false"].
|
||||
Extraction eq_nat_dec'.
|
||||
|
||||
(* We can build "smart" versions of the usual Boolean operators and put them to
|
||||
* good use in certified programming. For instance, here is a [sumbool] version
|
||||
* of Boolean "or." *)
|
||||
|
||||
Notation "x || y" := (if x then Yes else Reduce y).
|
||||
|
||||
(* Let us use it for building a function that decides list membership. We need
|
||||
* to assume the existence of an equality decision procedure for the type of
|
||||
* list elements. *)
|
||||
|
||||
Section In_dec.
|
||||
Variable A : Set.
|
||||
Variable A_eq_dec : forall x y : A, {x = y} + {x <> y}.
|
||||
|
||||
(* The final function is easy to write using the techniques we have developed
|
||||
* so far. *)
|
||||
|
||||
Definition In_dec : forall (x : A) (ls : list A), {In x ls} + {~ In x ls}.
|
||||
refine (fix f (x : A) (ls : list A) : {In x ls} + {~ In x ls} :=
|
||||
match ls with
|
||||
| nil => No
|
||||
| x' :: ls' => A_eq_dec x x' || f x ls'
|
||||
end); simplify; equality.
|
||||
Defined.
|
||||
End In_dec.
|
||||
|
||||
Compute In_dec eq_nat_dec 2 (1 :: 2 :: nil).
|
||||
Compute In_dec eq_nat_dec 3 (1 :: 2 :: nil).
|
||||
|
||||
(* The [In_dec] function has a reasonable extraction to OCaml. *)
|
||||
|
||||
Extraction In_dec.
|
||||
|
||||
(* This is more or the less code for the corresponding function from the OCaml
|
||||
* standard library. *)
|
||||
|
||||
|
||||
(** * Partial Subset Types *)
|
||||
|
||||
(* Our final implementation of dependent predecessor used a very specific
|
||||
* argument type to ensure that execution could always complete normally.
|
||||
* Sometimes we want to allow execution to fail, and we want a more principled
|
||||
* way of signaling failure than returning a default value, as [pred] does for
|
||||
* [0]. One approach is to define this type family [maybe], which is a version
|
||||
* of [sig] that allows obligation-free failure. *)
|
||||
|
||||
Inductive maybe (A : Set) (P : A -> Prop) : Set :=
|
||||
| Unknown : maybe P
|
||||
| Found : forall x : A, P x -> maybe P.
|
||||
|
||||
(* We can define some new notations, analogous to those we defined for subset
|
||||
* types. *)
|
||||
|
||||
Notation "{{ x | P }}" := (maybe (fun x => P)).
|
||||
Notation "??" := (Unknown _).
|
||||
Notation "[| x |]" := (Found _ x _).
|
||||
|
||||
(* Now our next version of [pred] is trivial to write. *)
|
||||
|
||||
Definition pred_strong7 : forall n : nat, {{m | n = S m}}.
|
||||
refine (fun n =>
|
||||
match n return {{m | n = S m}} with
|
||||
| O => ??
|
||||
| S n' => [|n'|]
|
||||
end); trivial.
|
||||
Defined.
|
||||
|
||||
Compute pred_strong7 2.
|
||||
Compute pred_strong7 0.
|
||||
|
||||
(* Because we used [maybe], one valid implementation of the type we gave
|
||||
* [pred_strong7] would return [??] in every case. We can strengthen the type
|
||||
* to rule out such vacuous implementations, and the type family [sumor] from
|
||||
* the standard library provides the easiest starting point. For type [A] and
|
||||
* proposition [B], [A + {B}] desugars to [sumor A B], whose values are either
|
||||
* values of [A] or proofs of [B]. *)
|
||||
|
||||
Print sumor.
|
||||
|
||||
(* We add notations for easy use of the [sumor] constructors. The second
|
||||
* notation is specialized to [sumor]s whose [A] parameters are instantiated
|
||||
* with regular subset types, since this is how we will use [sumor] below. *)
|
||||
|
||||
Notation "!!" := (inright _ _).
|
||||
Notation "[|| x ||]" := (inleft _ [x]).
|
||||
|
||||
(* Now we are ready to give the final version of possibly failing predecessor.
|
||||
* The [sumor]-based type that we use is maximally expressive; any
|
||||
* implementation of the type has the same input-output behavior. *)
|
||||
|
||||
Definition pred_strong8 : forall n : nat, {m : nat | n = S m} + {n = 0}.
|
||||
refine (fun n =>
|
||||
match n with
|
||||
| O => !!
|
||||
| S n' => [||n'||]
|
||||
end); trivial.
|
||||
Defined.
|
||||
|
||||
Compute pred_strong8 2.
|
||||
Compute pred_strong8 0.
|
||||
|
||||
(* As with our other maximally expressive [pred] function, we arrive at quite
|
||||
* simple output values, thanks to notations. *)
|
||||
|
||||
|
||||
(** * Monadic Notations *)
|
||||
|
||||
(* We can treat [maybe] like a monad, in the same way that the Haskell [Maybe]
|
||||
* type is interpreted as a failure monad. Our [maybe] has the wrong type to be
|
||||
* a literal monad, but a "bind"-like notation will still be helpful. *)
|
||||
|
||||
Notation "x <- e1 ; e2" := (match e1 with
|
||||
| Unknown => ??
|
||||
| Found x _ => e2
|
||||
end)
|
||||
(right associativity, at level 60).
|
||||
|
||||
(* The meaning of [x <- e1; e2] is: First run [e1]. If it fails to find an
|
||||
* answer, then announce failure for our derived computation, too. If [e1]
|
||||
* _does_ find an answer, pass that answer on to [e2] to find the final result.
|
||||
* The variable [x] can be considered bound in [e2].
|
||||
*
|
||||
* This notation is very helpful for composing richly typed procedures. For
|
||||
* instance, here is a very simple implementation of a function to take the
|
||||
* predecessors of two naturals at once. *)
|
||||
|
||||
Definition doublePred : forall n1 n2 : nat, {{p | n1 = S (fst p) /\ n2 = S (snd p)}}.
|
||||
refine (fun n1 n2 =>
|
||||
m1 <- pred_strong7 n1;
|
||||
m2 <- pred_strong7 n2;
|
||||
[|(m1, m2)|]); propositional.
|
||||
Defined.
|
||||
|
||||
(* We can build a [sumor] version of the "bind" notation and use it to write a
|
||||
* similarly straightforward version of this function. *)
|
||||
|
||||
Notation "x <-- e1 ; e2" := (match e1 with
|
||||
| inright _ => !!
|
||||
| inleft (exist x _) => e2
|
||||
end)
|
||||
(right associativity, at level 60).
|
||||
|
||||
Definition doublePred' : forall n1 n2 : nat,
|
||||
{p : nat * nat | n1 = S (fst p) /\ n2 = S (snd p)}
|
||||
+ {n1 = 0 \/ n2 = 0}.
|
||||
refine (fun n1 n2 =>
|
||||
m1 <-- pred_strong8 n1;
|
||||
m2 <-- pred_strong8 n2;
|
||||
[||(m1, m2)||]); propositional.
|
||||
Defined.
|
||||
|
||||
(* This example demonstrates how judicious selection of notations can hide
|
||||
* complexities in the rich types of programs. *)
|
||||
|
||||
|
||||
(** * A Type-Checking Example *)
|
||||
|
||||
(* We can apply these specification types to build a certified type checker for
|
||||
* a simple expression language. *)
|
||||
|
||||
Inductive exp :=
|
||||
| Nat (n : nat)
|
||||
| Plus (e1 e2 : exp)
|
||||
| Bool (b : bool)
|
||||
| And (e1 e2 : exp).
|
||||
|
||||
(* We define a simple language of types and its typing rules. *)
|
||||
|
||||
Inductive type := TNat | TBool.
|
||||
|
||||
Inductive hasType : exp -> type -> Prop :=
|
||||
| HtNat : forall n,
|
||||
hasType (Nat n) TNat
|
||||
| HtPlus : forall e1 e2,
|
||||
hasType e1 TNat
|
||||
-> hasType e2 TNat
|
||||
-> hasType (Plus e1 e2) TNat
|
||||
| HtBool : forall b,
|
||||
hasType (Bool b) TBool
|
||||
| HtAnd : forall e1 e2,
|
||||
hasType e1 TBool
|
||||
-> hasType e2 TBool
|
||||
-> hasType (And e1 e2) TBool.
|
||||
|
||||
(* It will be helpful to have a function for comparing two types. We build one
|
||||
* using [decide equality]. *)
|
||||
|
||||
Definition eq_type_dec : forall t1 t2 : type, {t1 = t2} + {t1 <> t2}.
|
||||
decide equality.
|
||||
Defined.
|
||||
|
||||
(* Another notation complements the monadic notation for [maybe] that we defined
|
||||
* earlier. Sometimes we want to include "assertions" in our procedures. That
|
||||
* is, we want to run a decision procedure and fail if it fails; otherwise, we
|
||||
* want to continue, with the proof that it produced made available to us. This
|
||||
* infix notation captures that idea, for a procedure that returns an arbitrary
|
||||
* two-constructor type. *)
|
||||
|
||||
Notation "e1 ;; e2" := (if e1 then e2 else ??)
|
||||
(right associativity, at level 60).
|
||||
|
||||
(* With that notation defined, we can implement a [typeCheck] function, whose
|
||||
* code is only more complex than what we would write in ML because it needs to
|
||||
* include some extra type annotations. Every [[|e|]] expression adds a
|
||||
* [hasType] proof obligation, and [eauto] makes short work of them when we add
|
||||
* [hasType]'s constructors as hints. *)
|
||||
|
||||
Hint Constructors hasType.
|
||||
|
||||
Definition typeCheck : forall e : exp, {{t | hasType e t}}.
|
||||
refine (fix F (e : exp) : {{t | hasType e t}} :=
|
||||
match e return {{t | hasType e t}} with
|
||||
| Nat _ => [|TNat|]
|
||||
| Plus e1 e2 =>
|
||||
t1 <- F e1;
|
||||
t2 <- F e2;
|
||||
eq_type_dec t1 TNat;;
|
||||
eq_type_dec t2 TNat;;
|
||||
[|TNat|]
|
||||
| Bool _ => [|TBool|]
|
||||
| And e1 e2 =>
|
||||
t1 <- F e1;
|
||||
t2 <- F e2;
|
||||
eq_type_dec t1 TBool;;
|
||||
eq_type_dec t2 TBool;;
|
||||
[|TBool|]
|
||||
end); subst; eauto.
|
||||
Defined.
|
||||
|
||||
(* Despite manipulating proofs, our type checker is easy to run. *)
|
||||
|
||||
Compute typeCheck (Nat 0).
|
||||
Compute typeCheck (Plus (Nat 1) (Nat 2)).
|
||||
Compute typeCheck (Plus (Nat 1) (Bool false)).
|
||||
|
||||
(* The type checker also extracts to some reasonable OCaml code. *)
|
||||
|
||||
Extraction typeCheck.
|
||||
|
||||
(* We can adapt this implementation to use [sumor], so that we know our type-checker
|
||||
* only fails on ill-typed inputs. First, we define an analogue to the
|
||||
* "assertion" notation. *)
|
||||
|
||||
Notation "e1 ;;; e2" := (if e1 then e2 else !!)
|
||||
(right associativity, at level 60).
|
||||
|
||||
(* Next, we prove a helpful lemma, which states that a given expression can have
|
||||
* at most one type. *)
|
||||
|
||||
Lemma hasType_det : forall e t1,
|
||||
hasType e t1
|
||||
-> forall t2, hasType e t2
|
||||
-> t1 = t2.
|
||||
Proof.
|
||||
induct 1; invert 1; equality.
|
||||
Qed.
|
||||
|
||||
(* Now we can define the type-checker. Its type expresses that it only fails on
|
||||
* untypable expressions. *)
|
||||
|
||||
Hint Resolve hasType_det.
|
||||
(* The lemma [hasType_det] will also be useful for proving proof obligations
|
||||
* with contradictory contexts. *)
|
||||
|
||||
Definition typeCheck' : forall e : exp, {t : type | hasType e t} + {forall t, ~ hasType e t}.
|
||||
(* Finally, the implementation of [typeCheck] can be transcribed literally,
|
||||
* simply switching notations as needed. *)
|
||||
|
||||
refine (fix F (e : exp) : {t : type | hasType e t} + {forall t, ~ hasType e t} :=
|
||||
match e return {t : type | hasType e t} + {forall t, ~ hasType e t} with
|
||||
| Nat _ => [||TNat||]
|
||||
| Plus e1 e2 =>
|
||||
t1 <-- F e1;
|
||||
t2 <-- F e2;
|
||||
eq_type_dec t1 TNat;;;
|
||||
eq_type_dec t2 TNat;;;
|
||||
[||TNat||]
|
||||
| Bool _ => [||TBool||]
|
||||
| And e1 e2 =>
|
||||
t1 <-- F e1;
|
||||
t2 <-- F e2;
|
||||
eq_type_dec t1 TBool;;;
|
||||
eq_type_dec t2 TBool;;;
|
||||
[||TBool||]
|
||||
end); simplify; propositional; subst; eauto;
|
||||
match goal with
|
||||
| [ H : hasType _ _ |- _ ] => invert2 H
|
||||
end; eauto.
|
||||
Defined.
|
||||
|
||||
(* The short implementation here hides just how time-saving automation is.
|
||||
* Every use of one of the notations adds a proof obligation, giving us 12 in
|
||||
* total. Most of these obligations require inversions and either uses of
|
||||
* [hasType_det] or applications of [hasType] rules.
|
||||
*
|
||||
* Our new function remains easy to test: *)
|
||||
|
||||
Compute typeCheck' (Nat 0).
|
||||
Compute typeCheck' (Plus (Nat 1) (Nat 2)).
|
||||
Compute typeCheck' (Plus (Nat 1) (Bool false)).
|
||||
|
||||
(* The results of simplifying calls to [typeCheck'] look deceptively similar to
|
||||
* the results for [typeCheck], but now the types of the results provide more
|
||||
* information. *)
|
|
@ -7,6 +7,7 @@ Invariant.v
|
|||
ModelCheck.v
|
||||
Imp.v
|
||||
AbstractInterpret.v
|
||||
FrapWithoutSets.v
|
||||
Frap.v
|
||||
BasicSyntax_template.v
|
||||
BasicSyntax.v
|
||||
|
@ -31,6 +32,7 @@ LogicProgramming_template.v
|
|||
AbstractInterpretation.v
|
||||
CompilerCorrectness.v
|
||||
CompilerCorrectness_template.v
|
||||
SubsetTypes.v
|
||||
LambdaCalculusAndTypeSoundness_template.v
|
||||
LambdaCalculusAndTypeSoundness.v
|
||||
TypesAndMutation.v
|
||||
|
|
Loading…
Reference in a new issue