diff options
Diffstat (limited to 'examples/equality.makkai')
| -rw-r--r-- | examples/equality.makkai | 30 |
1 files changed, 27 insertions, 3 deletions
diff --git a/examples/equality.makkai b/examples/equality.makkai index 5e9a0f9..86b81ae 100644 --- a/examples/equality.makkai +++ b/examples/equality.makkai @@ -1,9 +1,11 @@ +// basic prelude let set Empty = variant[] let set Unit = record {} let element pt : Unit = {} - +// Bool is not inductive let set Two = variant [ zero : Unit | one : Unit] +// the main thrust let signature SetWithEquivRelation = theory { Carrier :: Set, Relation :: (x : set-of(Carrier)) (y: set-of(Carrier)) -> Set, @@ -15,6 +17,8 @@ let signature SetWithEquivRelation = theory { -> <set-of(Relation x z)> } + +// by cases we construct this on Two let instance eqTwo :: SetWithEquivRelation = { .Carrier = Two :: Set, .Relation = for (x: Two) (y: Two), @@ -25,7 +29,7 @@ let instance eqTwo :: SetWithEquivRelation = { case x of [ zero. _ => case y of [ zero. _ => <r> | one. _ => <r> ] | one. _ => case y of [ zero. _ => <r> | one. _ => <r> ] ], .Transitive = for (x: Two)(y: Two)(z: Two)(r: set-of(Relation x y))(s: set-of(Relation y z)), - case x of [ zero. _ => case y of + case x of [ zero. _ => case y of // there are choices here to use <r> or <s> in places that are irrelevant [ zero. _ => case z of [ zero. _ => <r> | one. _ => <s> ] | one. _ => case z of [ zero. _ => <pt>| one. _ => <r> ] ] | one. _ => case y of @@ -33,6 +37,26 @@ let instance eqTwo :: SetWithEquivRelation = { | one. _ => case z of [ zero. _ => <s> | one. _ => <r> ] ] ] } +// show off forming sets let set Diagonal = record { x : set-of(eqTwo .Carrier), y : set-of(eqTwo .Carrier), equal : set-of((eqTwo .Relation) x y) } - let element oneEqualsOne : Diagonal = { .x = one. pt, .y = one. pt, .equal = pt } + +// prove inequality +let instance zeroNeqOne + :: (r : set-of((eqTwo .Relation) (zero. pt) (one. pt))) -> <Empty> + = for (r : set-of((eqTwo .Relation) (zero. pt) (one. pt))), <r> + +// prove inequality the fun way +let signature NeqParticular = theory { + SE :: SetWithEquivRelation, + A :: <set-of(SE .Carrier)>, + B :: <set-of(SE .Carrier)>, + Neq :: (r: set-of((SE .Relation) (element-of(A)) (element-of(B)))) -> <Empty> +} + +let instance zeroNeqOne :: NeqParticular = { + .SE = eqTwo, + .A = <zero. pt>, + .B = <one. pt>, + .Neq = for (r: set-of((SE .Relation) (element-of(A)) (element-of(B)))), <r> +} |