proofs/sequence_membership.bend
stelliferous@0.0.3.0 · 102 lines · 0 definitions
1# A reusable finite-sequence witness; range membership yields a bounded index.
2import Base
3import stelliferous@0.0.3.0/ordered_matrix.bend as OrderedMatrix
4import stelliferous@0.0.3.0/proofs/ordered_ranges.bend as Ranges
5import stelliferous@0.0.3.0/proofs/natural_addition.bend as Addition
6import stelliferous@0.0.3.0/proofs/word_encoding.bend as WordEncoding
7import stelliferous@0.0.3.0/proofs/storage_shape.bend as Shape
8import stelliferous@0.0.3.0/proofs/nat_order.bend as Order
9
10def All(-Element: Data,-Property: Element -> Data,items: List<&2,Element>) -> Data:
11 match items:
12 case Nil{}: Unit
13 case item <> rest: Shape.Both<Property(item),All(Element,Property,rest)>
14
15# Construct finite range evidence from a bounded pointwise rule.
16def range_all(~Context: Data,~Property: @+context: Context -> @+index: Nat -> Data,~size: Context -> Nat,
17 ~cell: @+context: Context -> @+index: Nat -> @+inside: {Nat.is_lt(index,size(context)) == True{} : Bool} -> Property(context,index),
18 remaining: Nat,+position: Nat,+context: Context,+room: {Nat.is_le(Nat.add(position,remaining),size(context)) == True{} : Bool}) ->
19 All(Nat,{index => Property(context,index) : Nat -> Data},Ranges.range(remaining,position)):
20 match remaining:
21 case 0n: Unit{}
22 case 1n+ +rest:
23 Shape.Both{cell(context,position,Order.room_index(position,rest,size(context),room)),
24 range_all(~Context,~Property,~size,~cell,rest,1n+position,context,Order.advance_room(position,rest,size(context),room))}
25
26def all_concatenated(-Element: Data,-Property: Element -> Data,+left: List<&2,Element>,+right: List<&2,Element>,
27 left_proof: All(Element,Property,left),right_proof: All(Element,Property,right)) -> All(Element,Property,OrderedMatrix.cat(Element,left,right)):
28 match left:
29 case Nil{}: right_proof
30 case +item <> +rest:
31 Shape.Both{head,tail} = left_proof
32 Shape.Both{head,all_concatenated(Element,Property,rest,right,tail,right_proof)}
33
34def transform_all(~Element: Data,~Context: Data,~Before: @+context: Context -> @+element: Element -> Data,~After: @+context: Context -> @+element: Element -> Data,
35 ~transform: @+context: Context -> @+element: Element -> @+evidence: Before(context,element) -> After(context,element),
36 +items: List<&2,Element>,+context: Context,evidence: All(Element,{element => Before(context,element) : Element -> Data},items)) ->
37 All(Element,{element => After(context,element) : Element -> Data},items):
38 match items:
39 case Nil{}: Unit{}
40 case +element <> +rest:
41 Shape.Both{head,tail} = evidence
42 Shape.Both{transform(context,element,head),transform_all(~Element,~Context,~Before,~After,~transform,rest,context,tail)}
43
44def Member(-A: Data,+value: A,values: List<&2,A>) -> Data:
45 match values:
46 case Nil{}: Empty
47 case head <> rest: Either<&2,&2,{value == head : A},Member(A,value,rest)>
48
49def all_member(-Element: Data,-Property: Element -> Data,+value: Element,items: List<&2,Element>,
50 all: All(Element,Property,items),member: Member(Element,value,items)) -> Property(value):
51 match items:
52 case []: Empty.absurd(Property(value),member)
53 case +head <> +rest:
54 Shape.Both{head_proof,tail_proof} = all
55 match member:
56 case Inl{equal}:
57 %Equal.sym(Element,value,head,equal) : Property(_)
58 head_proof
59 case Inr{tail}: all_member(Element,Property,value,rest,tail_proof,tail)
60
61def lift_split(-A: Data,+value: A,+head: A,+left: List<&2,A>,+right: List<&2,A>,
62 choice: Either<&2,&2,Member(A,value,left),Member(A,value,right)>) -> Either<&2,&2,Member(A,value,head <> left),Member(A,value,right)>:
63 match choice:
64 case Inl{member}: Inl{Inr{member}}
65 case Inr{member}: Inr{member}
66
67def split_concatenated(-A: Data,+value: A,+left: List<&2,A>,+right: List<&2,A>,member: Member(A,value,OrderedMatrix.cat(A,left,right))) ->
68 Either<&2,&2,Member(A,value,left),Member(A,value,right)>:
69 match left:
70 case Nil{}: Inr{member}
71 case +head <> +rest:
72 match member:
73 case Inl{equal}: Inl{Inl{equal}}
74 case Inr{tail}: lift_split(A,value,head,rest,right,split_concatenated(A,value,rest,right,tail))
75
76def range_member(+count: Nat,+start: Nat,+index: Nat,inside: {Nat.is_lt(index,count) == True{} : Bool}) ->
77 Member(Nat,Nat.add(start,index),Ranges.range(count,start)):
78 match count index:
79 case 0n 0n: Empty.absurd(Member(Nat,Nat.add(start,0n),[]),WordEncoding.false_true(inside))
80 case 0n 1n+index: Empty.absurd(Member(Nat,Nat.add(start,1n+index),[]),WordEncoding.false_true(inside))
81 case 1n+rest 0n: Inl{Addition.zero_right(start)}
82 case 1n+ +rest 1n+ +previous:
83 Inr{
84 %Equal.sym(Nat,Nat.add(start,1n+previous),1n+Nat.add(start,previous),Addition.successor_right(start,previous)) : Member(Nat,_,Ranges.range(rest,1n+start))
85 range_member(rest,1n+start,previous,inside)}
86
87type RangeIndex<-count: Nat,-start: Nat,-value: Nat> is Data:
88 RangeIndex{index: Nat,inside: {Nat.is_lt(index,count) == True{} : Bool},exact: {Nat.add(start,index) == value : Nat}}
89
90def lift_range_index(+count: Nat,+start: Nat,+value: Nat,proof: RangeIndex<count,1n+start,value>) -> RangeIndex<1n+count,start,value>:
91 RangeIndex{+index,inside,exact} = proof
92 RangeIndex{1n+index,inside,
93 Equal.trans(Nat,Nat.add(start,1n+index),1n+Nat.add(start,index),value,Addition.successor_right(start,index),exact)}
94
95def range_index(+count: Nat,+start: Nat,+value: Nat,member: Member(Nat,value,Ranges.range(count,start))) -> RangeIndex<count,start,value>:
96 match count:
97 case 0n: Empty.absurd(RangeIndex<0n,start,value>,member)
98 case 1n+ +rest:
99 match member:
100 case Inl{equal}:
101 RangeIndex{0n,{==},Equal.trans(Nat,Nat.add(start,0n),start,value,Addition.zero_right(start),Equal.sym(Nat,value,start,equal))}
102 case Inr{tail}: lift_range_index(rest,start,value,range_index(rest,1n+start,value,tail))