val bool_or_monoid:monoid bool
let bool_or_monoid : monoid bool =
  let or_ b1 b2 = b1 || b2 in
  intro_monoid bool false or_
val bool_or_monoid:monoid bool
let bool_or_monoid:monoid bool =
let or_ b1 b2 = b1 || b2 in
intro_monoid bool false or_
FStar.Algebra.Monoid.fst.checked
prims.fst.checked FStar.PropositionalExtensionality.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
FStar.Algebra.Monoid.fst
FStar.Algebra.Monoid.intro_monoid Prims.bool Prims.op_BarBar
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module FStar.Algebra.Monoid

open FStar.Classical
module PropExt = FStar.PropositionalExtensionality

(*
 * AR: 05/12: adding calls to equational lemmas from PropositionalExtensionality
 *            these should go away with proper prop support
 *            also see the comment in PropositionalExtensionality.fst
 *)

(** Definition of a monoid *)

let right_unitality_lemma (m:Type) (u:m) (mult:m -> m -> m) =
  forall (x:m). x `mult` u == x

let left_unitality_lemma (m:Type) (u:m) (mult:m -> m -> m) =
  forall (x:m). u `mult` x == x

let associativity_lemma (m:Type) (mult:m -> m -> m) =
  forall (x y z:m). x `mult` y `mult` z == x `mult` (y `mult` z)

unopteq
type monoid (m:Type) =
  | Monoid :
    unit:m ->
    mult:(m -> m -> m) ->
    right_unitality:squash (right_unitality_lemma m unit mult) ->
    left_unitality:squash (left_unitality_lemma m unit mult) ->
    associativity:squash (associativity_lemma m mult) ->
    monoid m


let intro_monoid (m:Type) (u:m) (mult:m -> m -> m)
  : Pure (monoid m)
    (requires (right_unitality_lemma m u mult /\ left_unitality_lemma m u mult /\ associativity_lemma m mult))
    (ensures (fun mm -> Monoid?.unit mm == u /\ Monoid?.mult mm == mult))
=
  Monoid u mult () () ()


(** Some monoid structures *)

let nat_plus_monoid : monoid nat =
  let add (x y : nat) : nat = x + y in
  intro_monoid nat 0 add

let int_plus_monoid : monoid int =
  intro_monoid int 0 (+)

(* let int_mul_monoid : monoid int = *)
(*   intro_monoid int 1 op_Multiply *)

let conjunction_monoid : monoid prop =
  let u : prop = singleton True in
  let mult (p q : prop) : prop = p /\ q in

  let left_unitality_helper (p:prop) : Lemma ((u `mult` p) == p) =
    assert ((u `mult` p) <==> p) ;
    PropExt.apply (u `mult` p) p
  in

  let right_unitality_helper (p:prop) : Lemma ((p `mult` u) == p) =
    assert ((p `mult` u) <==> p) ;
    PropExt.apply (p `mult` u) p
  in

  let associativity_helper (p1 p2 p3 : prop) : Lemma (p1 `mult` p2 `mult` p3 == p1 `mult` (p2 `mult` p3)) =
    assert (p1 `mult` p2 `mult` p3 <==> p1 `mult` (p2 `mult` p3)) ;
    PropExt.apply (p1 `mult` p2 `mult` p3) (p1 `mult` (p2 `mult` p3))
  in

  forall_intro right_unitality_helper ;
  assert (right_unitality_lemma prop u mult) ;
  forall_intro left_unitality_helper ;
  assert (left_unitality_lemma prop u mult) ;
  forall_intro_3 associativity_helper;
  assert (associativity_lemma prop mult) ;
  intro_monoid prop u mult


let disjunction_monoid : monoid prop =
  let u : prop = singleton False in
  let mult (p q : prop) : prop = p \/ q in

  let left_unitality_helper (p:prop) : Lemma ((u `mult` p) == p) =
    assert ((u `mult` p) <==> p) ;
    PropExt.apply (u `mult` p) p
  in

  let right_unitality_helper (p:prop) : Lemma ((p `mult` u) == p) =
    assert ((p `mult` u) <==> p) ;
    PropExt.apply (p `mult` u) p
  in

  let associativity_helper (p1 p2 p3 : prop) : Lemma (p1 `mult` p2 `mult` p3 == p1 `mult` (p2 `mult` p3)) =
    assert (p1 `mult` p2 `mult` p3 <==> p1 `mult` (p2 `mult` p3)) ;
    PropExt.apply (p1 `mult` p2 `mult` p3) (p1 `mult` (p2 `mult` p3))
  in

  forall_intro right_unitality_helper ;
  assert (right_unitality_lemma prop u mult) ;
  forall_intro left_unitality_helper ;
  assert (left_unitality_lemma prop u mult) ;
  forall_intro_3 associativity_helper;
  assert (associativity_lemma prop mult) ;
  intro_monoid prop u mult

let bool_and_monoid : monoid bool =
  let and_ b1 b2 = b1 && b2 in
  intro_monoid bool true and_
val bool_or_monoid:monoid bool
FStar.Algebra.Monoid.monoid Prims.bool