sig higher-order.
kind a, alist type.
type anil alist.
type acons a -> alist -> alist.
type mappred (a -> a -> o) -> alist -> alist -> o.
type swap (a -> a -> o) -> (a -> a -> o).
type star (a -> a -> o) -> (a -> a -> o).
% We don't have these explicitly in Abella, but we can define them
type and o -> o -> o.
type exist (a -> o) -> o.
module higher-order. exist P :- P X. and P Q :- P, Q. mappred P anil anil. mappred P (acons X XS) (acons Y YS) :- P X Y, mappred P XS YS. swap P X Y :- P Y X. star P X X. star P X Y :- P X Z, star P Z Y.
Click on a command or tactic to see a detailed view of its use.
%% %% This development is currently limited by the lack of polymorphism Specification "higher-order". Theorem split : forall R S L K, {mappred (x\ y\ exist z\ and (R x z) (S z y)) L K} -> exists J, {mappred R L J} /\ {mappred S J K}. Theorem combine : forall R S L K J, {mappred R L J} -> {mappred S J K} -> {mappred (x\ y\ exist z\ and (R x z) (S z y)) L K}. Theorem deterministic : forall R L K1 K2, (forall X Y1 Y2, {R X Y1} -> {R X Y2} -> Y1 = Y2) -> {mappred R L K1} -> {mappred R L K2} -> K1 = K2.induction on 2. intros. case H2. case H3. search. case H3. apply H1 to H4 H6. apply IH to H1 H5 H7. search.Theorem swap1 : forall R L K, {mappred (swap R) L K} -> {mappred R K L}. Theorem swap2 : forall R L K, {mappred R K L} -> {mappred (swap R) L K}. Define reflexive : (a -> a -> o) -> prop by reflexive P := forall X, {P X X}. Define transitive : (a -> a -> o) -> prop by transitive P := forall X Y Z, {P X Y} -> {P Y Z} -> {P X Z}. Theorem star_reflexive : forall P, reflexive (star P). Theorem star_transitive : forall P, transitive (star P). Define contained_in : (a -> a -> o) -> (a -> a -> o) -> prop by contained_in P S := forall X Y, {P X Y} -> {S X Y}. % Theorem: star is minimal -- any reflexive and transitive relation % which contains P must contain (star P). Theorem star_minimal : forall P S, contained_in P S -> reflexive S -> transitive S -> contained_in (star P) S.intros. unfold. induction on 1. intros. case H4. case H2. backchain H5. apply IH to H6. case H1. apply H8 to H5. case H3. apply H10 to H9 H7. search.% Corollary: if P is reflexive and transitive then (star P) equals P. % The easy direction is that (star P) contains P. The harder % direction is showing that P contains (star P). We do this harder % direction here. Theorem star_vacuous : forall P, reflexive P -> transitive P -> contained_in (star P) P. % Corollary: star is idempotent Theorem star_idempotent : forall P, contained_in (star (star P)) (star P).