Add_assoc

[Pytheas01]

Hello,
how would you defined the add_assoc function below, in F*?
Many thanks.
P

open FStar.Math.Lemmas
let nat_add_monoid : monoid nat =
  {
    op = (+);
    unit = 0;

    assoc = (fun x y z -> add_assoc x y z);
    left_id = (fun x -> add_0_left x);
    right_id = (fun x -> add_0_right x);
  }

[mtzguido]

I'm not sure I understand the question. Are you asking how to prove that addition of nats is associative? This is trivial by using the SMT solver, so you can define a lemma like

let add_assoc (x y z : nat) : Lemma ((x+y)+z == x+(y+z)) = ()

Or probably just replace add_assoc x y z with () in your record definition, to prove it on the spot. For more complicated facts, where the SMT can't automatically figure it out, you could do a proof by induction.

[Pytheas01]

Hi,
how would you do a proof by induction? The Solver can't solve left_id.

module Monoid0

open FStar.Math.Lemmas

noeq 
type monoid (a:Type) = {
  mempty : a;
  mappend : a -> a -> a;

  left_id  : x:a -> mappend mempty x == x;
  right_id : x:a -> mappend x mempty == x;
  assoc    : x:a -> y:a -> z:a ->
               mappend x (mappend y z) == mappend (mappend x y) z;
}

let int_add_monoid : monoid int =
  {
    mempty = 0;
    mappend = (+);

    left_id =  (fun x -> ());
    right_id = (fun x -> ());
    assoc = (fun x y z -> ());
  }

[nikswamy]

See https://fstar-lang.org/tutorial/book/part1/part1_lemmas.html#lemmas-and-proofs-by-induction