Calling lemma via apply_lemma fails in manual case (line 115)

MinimalApplyLemmaBugReproduction.fst

module MinimalApplyLemmaBugReproduction

open FStar.Tactics.V2
open FStar.List
open FStar.List.Tot

noeq type setoid_monoid (a: Type) = {
  eq: a -> a -> Type;
  op: a -> a -> a;  
  id: a;   
  associativity: x:a -> y:a -> z:a -> Lemma(eq (op x (op y z)) (op (op x y) z));
}

type monoid_mul #a (m: setoid_monoid a) = (mul: (a -> a -> a){mul == m.op})
type monoid_eq #a (m: setoid_monoid a) = (eq: (a -> a -> Type){eq == m.eq})

let term_equal (t1 t2: term) : Tac bool =
  let env = cur_env() in
  let t1_norm = norm_term [primops; iota; zeta; delta_attr ["unfold"]; delta] t1 in
  let t2_norm = norm_term [primops; iota; zeta; delta_attr ["unfold"]; delta] t2 in
  term_eq t1_norm t2_norm

let rec get_app_as_list (t: term) (op1 op2: term) : Tac (list term) =
  match inspect t with
  | Tv_App f (arg, q) -> 
      if (term_to_string f = "squash") then get_app_as_list arg op1 op2
      else if term_equal f op1 then f::[arg]
      else if term_equal f op2 then f::[arg]
      else (get_app_as_list f op1 op2)@[arg]
  | _ -> [t]

noeq type binary_or_unary_op = 
  | BinOp : (op: term) -> (lhs: term) -> (rhs: term) -> binary_or_unary_op
  | UnOp : (op: term) -> (arg: term) -> binary_or_unary_op
  | Atom : (term) -> binary_or_unary_op

let op_inspect (op: term) (op1 op2:term) : Tac binary_or_unary_op =
  match inspect (maybe_unsquash_term op) with
  | Tv_App _ _ -> 
                  (match get_app_as_list op op1 op2 with
                  | [a1; a2; a3; a4] -> fail ("Too many arguments: (" ^ term_to_string a1 ^ ", " ^ term_to_string a2 ^ ", " ^ term_to_string a3 ^ ", " ^ term_to_string a4 ^ ")")
                  | [o; a1; a2] -> BinOp o a1 a2
                  //| [o; a1] -> UnOp o a1
                  | _ -> Atom op)
  | _ -> Atom op

let term_name_of (t: term) : Tac string =
  match inspect t with
  | Tv_FVar fv -> flatten_name (inspect_fv fv) 
  | Tv_BVar namedv -> bv_to_string namedv
  | Tv_Var v -> term_to_string t
  | _ -> term_to_string t

let symbol_name_of x : Tac string =
  let ty = quote x in
  match inspect ty with
  | Tv_FVar fv -> 
      let name = flatten_name (inspect_fv fv) in
      name
  | Tv_BVar namedv -> bv_to_string namedv
  | Tv_Var v -> term_to_string ty
  | _ -> fail "Could not extract type name" 





let apply_associativity_auto_args #t (m: setoid_monoid t) : Tac unit =
    let atype = quote t in
    let mon_mul =  quote m.op in
    let mon_eq = quote m.eq in
    let insp_term term = op_inspect term mon_eq mon_mul in
    match insp_term (maybe_unsquash_term (cur_goal())) with
    | BinOp op lhs rhs ->
        let lhs_app = get_app_as_list lhs mon_eq mon_mul in
        let rhs_app = get_app_as_list rhs mon_eq mon_mul in
        if term_equal op (quote m.eq)
        then begin match (lhs_app, rhs_app) with
          | ([mul1; a; b], [mul2; c; d]) -> if term_equal mul1 mul2 then
          begin match (insp_term a, insp_term b, insp_term c, insp_term d) with
            | (BinOp innerLeft ia ib, _, _, BinOp innerRight ic id) 
              -> fail "not implemented yet"   
            | (Atom la, BinOp innerLeft ia ib, BinOp innerRight ic id, Atom ra) ->                
              let x = la in
              let y = ia in
              let z = ib in
              apply_lemma (quote (m.associativity)) 
            | _ -> fail "Not implemented yet"
          end
          | _ -> fail "left and right hand expressions are not both the monoid operation"
          end else fail "the goal is not the monoid equivalence expression"
    | _ -> fail "the goal should be a binary operator"
        
let apply_associativity_manual_args #t (m: setoid_monoid t) : Tac unit =
    let atype = quote t in
    let mon_mul =  quote m.op in
    let mon_eq = quote m.eq in
    let insp_term term = op_inspect term mon_eq mon_mul in
    match insp_term (maybe_unsquash_term (cur_goal())) with
    | BinOp op lhs rhs ->
        let lhs_app = get_app_as_list lhs mon_eq mon_mul in
        let rhs_app = get_app_as_list rhs mon_eq mon_mul in
        if term_equal op (quote m.eq)
        then begin match (lhs_app, rhs_app) with
          | ([mul1; a; b], [mul2; c; d]) -> if term_equal mul1 mul2 then
          begin match (insp_term a, insp_term b, insp_term c, insp_term d) with             
            | (Atom la, BinOp innerLeft ia ib, BinOp innerRight ic id, Atom ra) ->                
              let x = la in
              let y = ia in
              let z = ib in
              let inspect_assoc = (quote (m.associativity)) in                         
              let assoc_term = pack (Tv_App inspect_assoc (x, Q_Explicit)) in
              let assoc_term = pack (Tv_App assoc_term (y, Q_Explicit)) in
              let assoc_term = pack (Tv_App assoc_term (z, Q_Explicit)) in               
              apply_lemma assoc_term 
            | _ -> fail ("Not implemented yet")
          end else fail "left and right hand operators are not equal"
          | _ -> fail "both hands of the equation should be binary operators"
        end else fail "Top-level operator is not the monoid equivalence."
    | _ -> fail "Top-level operator should be a binary operator"
   
let example_proof 
  (a:Type)  
  (m: setoid_monoid a) 
  (mul: a->a->a{mul == m.op})
  (x y z: a)
  : Lemma (m.eq (m.op x (m.op y z)) (m.op (m.op x y) z))
  =
  assert(m.op x (m.op y z) `m.eq` (m.op (m.op x y) z)) by apply_associativity_auto_args m;
  assert(m.op x (m.op y z) `m.eq` (m.op (m.op x y) z)) by apply_associativity_manual_args m