Distributivity of Sequence Map over Function Composition in Dafny

lemma MapDistributivity(xs:seq<int>, f:int->int, g:int->int) requires forall x :: x in xs ==> f.requires(x); requires forall x :: x in xs ==> g.requires(f(x)); ensures forall x :: x in MapSeq(xs,f) ==> g.requires(x); ensures MapSeq(MapSeq(xs,f), g) == MapSeq(xs, Compose(f,g)); { if xs != [] { MapDistributivity(xs[1..], f, g); } } function Compose(f:int->int, g:int->int) : int->int { x reads f.reads(x) reads if f.requires(x) then g.reads(f(x)) else {} requires f.requires(x) requires g.requires(f(x)) -> g(f(x)) } function MapSeq(xs:seq<int>, f:int->int) : seq<int> reads MapSeqReads(xs, f); requires forall x :: x in xs ==> f.requires(x); ensures |xs| == |MapSeq(xs,f)|; ensures forall x :: x in xs ==> f(x) in MapSeq(xs,f); { if xs == [] then [] else [f(xs[0])] + MapSeq(xs[1..], f) } function MapSeqReads(xs:seq<int>, f:int->int) : set<object> reads if |xs| > 0 then f.reads(xs[0]) + MapSeqReads(xs[1..], f) else {}; decreases xs; ensures forall x :: x in xs ==> f.reads(x) <= MapSeqReads(xs,f); { if xs == [] then {} else f.reads(xs[0]) + MapSeqReads(xs[1..],f) } |