sum.mlw 868 Bytes
 Jean-Christophe Filliatre committed Nov 09, 2010 1   Guillaume Melquiond committed Dec 18, 2012 2 3 (** {1 Sum of the elements of an indexed container} *)  Guillaume Melquiond committed Jan 12, 2018 4 module Sum  Jean-Christophe Filliatre committed Jun 21, 2011 5   Andrei Paskevich committed Jun 15, 2018 6  use int.Int  Jean-Christophe Filliatre committed Nov 09, 2010 7 8 9  type container  Andrei Paskevich committed Jun 29, 2011 10  function f container int : int  Guillaume Melquiond committed Jun 14, 2018 11  (** f c i is the i-th element in the container c *)  Jean-Christophe Filliatre committed Nov 09, 2010 12   Andrei Paskevich committed Jun 29, 2011 13  function sum container int int : int  Guillaume Melquiond committed Jun 14, 2018 14  (** sum c i j is the sum \sum_{i <= k < j} f c k *)  Jean-Christophe Filliatre committed Nov 09, 2010 15 16 17 18 19 20 21 22  axiom Sum_def_empty : forall c : container, i j : int. j <= i -> sum c i j = 0 axiom Sum_def_non_empty : forall c: container, i j : int. i < j -> sum c i j = f c i + sum c (i+1) j lemma Sum_right_extension:  Jean-Christophe Filliatre committed Jun 21, 2011 23  forall c : container, i j : int.  Jean-Christophe Filliatre committed Nov 09, 2010 24 25 26 27 28 29 30  i < j -> sum c i j = sum c i (j-1) + f c (j-1) lemma Sum_transitivity : forall c : container, i k j : int. i <= k <= j -> sum c i j = sum c i k + sum c k j lemma Sum_eq :  Jean-Christophe Filliatre committed Jun 21, 2011 31  forall c1 c2 : container, i j : int.  Jean-Christophe Filliatre committed Nov 09, 2010 32 33 34  (forall k : int. i <= k < j -> f c1 k = f c2 k) -> sum c1 i j = sum c2 i j end