Lean experiment

examples/1Bsemantics/Makefile

@@ -1,9 +1,9 @@
 
-#OTT=../../bin/ott
-OTT=ott
+OTT=../../bin/ott
+#OTT=ott
 
 l1: l1.ott
-	$(OTT) -pp_grammar -isa_syntax true l1.ott -o l1.tex -o l1.thy -o l1.lem -o l1.v
+	$(OTT) -pp_grammar -isa_syntax true l1.ott -o l1.tex -o l1.v -o l1.lean # -o l1.thy -o l1.lem 
 	$(OTT) -tex_wrap false l1.ott -o l1_nowrap.tex 
 	pdflatex l1.tex
 	lem l1.lem  -isa

examples/1Bsemantics/l1.ott

@@ -9,49 +9,68 @@ Open Scope string.
 
 }}
 
+embed {{ lean
+set_option linter.unusedVariables false
+
+open Option
+}}
+
 metavar n ::=
   {{ com Numeric literals }}
   {{ phantom }}
   {{ lex numeric }}
   {{ lem integer }}
+  {{ lean Int }}
   {{ coq Z }}
 
-metavar location, l ::= 
+metavar Location {{ lean Location }}, l ::= 
   {{ com Store locations }}
   {{ lem string }}
+  {{ coq stringb }}
+  {{ lean String }}
+  {{ lean-equality }}
+
+% think idiomatic Lean to capitalise that, but with `metavar location {{ lean Location }}` it hits a bug in which the lean hom isn't respected in the inductive rule printing, so I've just capitalised the metavar for now - which will probably be bad for other targets
   {{ coq string }}
 
 grammar 
-b :: 'B_' ::=              {{ com booleans }}  {{ phantom }} {{ lem bool }} {{ coq bool }}
-  | true                    ::   :: true      {{ lem true }} {{ coq true }}
-  | false                   ::   :: false     {{ lem false }} {{ coq false }}
+b :: 'B_' ::=              {{ com booleans }}  {{ phantom }} {{ lem bool }} {{ coq bool }} {{ lean Bool }} 
+  | true                    ::   :: true      {{ lem true }} {{ coq true }} {{ lean true }}
+  | false                   ::   :: false     {{ lem false }} {{ coq false }} {{ lean false }}
 
-operations, op :: 'Op_' ::=            {{ com operations }}
+% is it nice to deeply embed the L1 bools like this or not?
+
+operations {{ lean Operations }}, op :: 'op_' ::=            {{ com operations }}
   | +                       ::   :: plus
   | >=                      ::   :: gteq
 
-e :: 'E_'  ::=	           {{ com expressions }}
+% all the other languages have constructors capitalised, but in Lean it seems conventional to have them lower-case. Ott doesn't support per-target constructor name prefixes, so in this file I've lower-cased them all for now.
+
+expr {{ lean Expr }}, e :: 'e_'  ::=	           {{ com expressions }}
   | n                       ::   :: num
   | b                       ::   :: bool
   | e1 op e2                ::   :: op
   | if e1 then e2 else e3   ::   :: if
-  | l := e                  ::   :: assign
+  | l := e1                 ::   :: assign
   | ! l                     ::   :: ref
   | skip                    ::   :: skip
   | e1 ; e2                 ::   :: sequence
   | while e1 do e2          ::   :: while
-  | ( e )                   :: M :: paren  {{ ichlo ([[e]]) }}
+  | ( e )                   :: M :: paren  {{ ichlo ([[e]]) }} {{ lean ([[e]]) }}
 
 v :: 'V_' ::=              {{ com values }}
   | n                       ::   :: num
   | b                       ::   :: bool
   | skip                    ::   :: skip    
 
-store , s :: 'Store_' ::=  {{ com stores }} {{ phantom }} {{ lem list (location * integer) }} {{ coq list (location * Z) }}
-   | empty                  ::   :: empty {{ lem [] }} {{ coq [] }}
-   | s , l |-> n            ::   :: extend  {{ lem (([[l]],[[n]])::[[s]]) }} {{ coq (([[l]],[[n]])::[[s]]) }}
+store {{ lean Store }}, s :: 'store_' ::=  {{ com stores }} {{ lem list (Location * integer) }} {{ coq list (Location * Z) }} {{ lean List (Location × Int) }}
+   | empty                  ::   :: empty {{ lem [] }} {{ coq [] }}  {{ lean [] }}
+   | s , l |-> n            ::   :: extend  {{ lem (([[l]],[[n]])::[[s]]) }} {{ coq (([[l]],[[n]])::[[s]]) }} {{ lean (([[l]],[[n]])::[[s]]) }}
 
-typ, T :: 'T_' ::=         {{ com types }}
+config {{ lean Config }}, c :: 'Config_' ::= {{ com configurations }} {{lem (expr*store) }} {{ coq (expr * store) }} {{ lean ([[Expr]] × [[Store]]) }}
+   | < e , s >              ::   :: config {{ lem ([[e]], [[s]]) }}  {{ coq ([[e]], [[s]]) }} {{ lean ([[e]], [[s]]) }}
+
+typ {{ lean Typ }}, T :: 't_' ::=         {{ com types }}
   | int                     ::   :: int
   | bool                    ::   :: bool
   | unit                    ::   :: unit
@@ -60,12 +79,12 @@ Tloc {{ isa tloc }} {{ coq tloc }} {{ hol tloc }} {{ lem tloc }} {{ ocaml tloc }
   | intref                  ::   :: intref	
 
 
-type_assumption, ta :: 'TA_' ::= {{ com type assumption }}
-  | l : Tloc                ::   :: loc
+type_assumption {{ lean Type_assumption }}, ta :: 'TA_' ::= {{ com type assumption }} {{ lean ([[Location]]×[[Tloc]]) }}
+  | l : Tloc                ::   :: loc {{ lean ([[l]], [[Tloc]]) }}
 
-G {{ tex \Gamma }} :: G_ ::=     {{ com type environments }} {{ phantom }} {{ lem list type_assumption }} {{ coq list type_assumption }}
-  | empty                   ::   :: empty {{ lem [] }}  {{ coq [] }}
-  | G , ta                  ::   :: extend {{ lem ([[ta]]::[[G]]) }}  {{ coq ([[ta]]::[[G]]) }}
+G {{ tex \Gamma }} :: G_ ::=     {{ com type environments }} {{ phantom }} {{ lem list type_assumption }} {{ coq list type_assumption }} {{ lean (List Type_assumption) }}
+  | empty                   ::   :: empty {{ lem [] }}  {{ coq [] }}  {{ lean [] }}
+  | G , ta                  ::   :: extend {{ lem ([[ta]]::[[G]]) }}  {{ coq ([[ta]]::[[G]]) }}  {{ lean ([[ta]]::[[G]]) }}
 
 
 terminals :: terminals_ ::=
@@ -78,19 +97,21 @@ terminals :: terminals_ ::=
   | <    :: :: la        {{ tex \langle }}
   | >    :: :: ra        {{ tex \rangle }}
 
+% for proof, would one really want subrules to generate functions, as Ott does, or more inductive relations?
+
 subrules
   v <:: e
 
 grammar 
 formula :: formula_ ::=
   | judgement              :: :: judgement
-  | n1 + n2 = n3           :: :: sum         {{ lem ([[n1]]+[[n2]]=[[n3]]) }}                               {{ coq ([[n1]]+[[n2]]=[[n3]]) }}                                 
-  | n1 >= n2 = b           :: :: leq         {{ lem ([[n1]]>=[[n2]]=[[b]]) }}                               {{ coq ([[n1]]>=[[n2]]=[[b]]) }}                                 
-  | s ( l ) = n            :: :: lookup      {{ lem (List.lookup [[l]] [[s]] =Just ([[n]])) }}              {{ coq (List.lookup [[l]] [[s]] =Just ([[n]])) }}                
-  | G ( l ) = Tloc         :: :: type_lookup {{ lem (lookup_location_type [[l]] [[G]] = Just ([[Tloc]])) }} {{ coq (lookup_location_type [[l]] [[G]] = Just ([[Tloc]])) }}     
+  | n1 + n2 = n3           :: :: sum         {{ lem ([[n1]]+[[n2]]=[[n3]]) }}                               {{ coq ([[n1]]+[[n2]]=[[n3]]) }}                                {{ lean ([[n1]]+[[n2]]=[[n3]]) }}                                    
+  | n1 >= n2 = b           :: :: leq         {{ lem ([[n1]]>=[[n2]]=[[b]]) }}                               {{ coq ([[n1]]>=[[n2]]=[[b]]) }}                                {{ lean (([[n1]]>=[[n2]])=[[b]]) }}                                    
+  | s ( l ) = n            :: :: lookup      {{ lem (List.lookup [[l]] [[s]] =Just ([[n]])) }}              {{ coq (List.lookup [[l]] [[s]] =Some ([[n]])) }}               {{ lean (List.lookup [[l]] [[s]] = some ([[n]])) }}                   
+  | G ( l ) = Tloc         :: :: type_lookup {{ lem (lookup_location_type [[l]] [[G]] = Just ([[Tloc]])) }} {{ coq (lookup_location_type [[l]] [[G]] = Some ([[Tloc]])) }}  {{ lean (List.lookup [[l]] [[G]] = some ([[Tloc]])) }}        
 
 
-% this is a bit ugly - to capture the different use of Gamma in L1 and L2 we have a list of a Lem variant type and two special-purpose lookup functions, with a wildcard pattern match in each.
+% this is a bit ugly - to capture the different use of Gamma in L1 and L2 we have a list of a Lem variant type and two special-purpose lookup functions, with a wildcard pattern match in each. Not currently implemented for Lean.
 
 embed {{ lem
 let rec lookup_location_type l g =
@@ -108,7 +129,7 @@ Jop :: '' ::=
 % Reductions. Want to allow lem hom to specify witness and animation info
 
 defn
-< e , s > -> < e' , s' > :: :: reduce :: ''  {{ com $\langle[[e]],\,[[s]]\rangle$ reduces to $\langle[[e']],\,[[s']]\rangle$ }} by
+c -> c' :: :: Reduce :: ''  {{ com $\langle[[e]],\,[[s]]\rangle$ reduces to $\langle[[e']],\,[[s']]\rangle$ }} by
 
   n1 + n2 = n
 ----------------------   :: op_plus
@@ -160,7 +181,7 @@ defn
 
 
 defn
-G |- e : T :: :: typing :: Ty_ by
+G |- e : T :: :: Typing :: ty_ by
 
 ------------------  :: int
   G |- n : int

revision_history.txt

@@ -581,3 +581,5 @@ Peter Sewell + Thibaut Pérami: Add "menhir-start-type" hom to specify the top l
 2024-12 @palmskog: only output plain comments in generated Coq code
 
 2024-12-30 Version 0.34
+
+2026-02-15 Peter Sewell: rudimentary Lean backend (generates well-typed Lean for examples/1Bsemantics/l1.ott; untested and probably broken for anything else)

src/auxl.ml

@@ -48,6 +48,7 @@ let mode_name m = match m with
   | Hol _ -> "HOL"
   | Lem _ -> "Lem"
   | Coq _ -> "Coq"
+  | Lean _ -> "Lean"
   | Twf _ -> "Twelf"
   | Caml _ -> "OCaml"
   | Lex _ -> "Lex"
@@ -602,6 +603,7 @@ let hom_name_for_pp_mode m
     | Isa _ -> "isa"
     | Hol _ -> "hol"
     | Lem _ -> "lem"
+    | Lean _ -> "lean"
     | Coq _ -> "coq"
     | Twf _ -> "twf"
     | Caml _ -> "ocaml"
@@ -818,6 +820,7 @@ let split3 (l : ('a * 'b * 'c) list) : 'a list * 'b list * 'c list =
 let big_line_comment m s = 
   match m with
   | Coq _ | Hol _ | Lem _ | Isa _ | Caml _ -> "(** "^s^" *)\n"
+  | Lean _ -> "/- - "^s^" - -/\n"
   | Twf _ -> "%%% "^s^" %%%\n\n"
   | Tex _ -> "% "^s^"\n"
   | Menhir _ | Lex _ | Ascii _ -> errorm m "big_line_comment"
@@ -1604,7 +1607,7 @@ let pp_true m in_prop =
       else "true"
   | Hol _ -> "T" 
   | Caml _ -> "true" 
-  | Lem _ -> "true" 
+  | Lem _ | Lean _ -> "true" 
   | Ascii _ | Tex _ | Twf _ | Lex _ | Menhir _ -> errorm m "pp_true"
 
 let pp_false m in_prop =
@@ -1616,7 +1619,7 @@ let pp_false m in_prop =
       else "false"
   | Hol _ -> "F" 
   | Caml _ -> "false"
-  | Lem _ -> "false"
+  | Lem _ | Lean _ -> "false"
   | Ascii _ | Tex _ | Twf _ | Lex _ | Menhir _ -> errorm m "pp_false"
 
 let pp_and m in_prop =
@@ -1629,6 +1632,7 @@ let pp_and m in_prop =
       then " /\\ "     
       else " && "
   | Hol _ -> " /\\ "
+  | Lean _ -> " /\\ "
   | Ascii _ | Tex _ | Twf _ | Lex _ | Menhir _ -> errorm m "pp_and"
 
 let pp_or m in_prop =
@@ -1639,6 +1643,7 @@ let pp_or m in_prop =
       then " \\/ "     
       else " || "
   | Hol _ -> " \\/ " 
+  | Lean _ -> " \\/ " 
   | Caml _ -> " || "
   | Lem _ -> " || "
   | Ascii _ | Tex _ | Twf _ | Lex _ | Menhir _ -> errorm m "pp_or"
@@ -1684,7 +1689,7 @@ let insert_append m l =
 	  ^ ( String.concat " <- " 
 	      (List.map2 (fun s nl -> s ^ " " ^ nl) l list_nl) )
 	  ^ final_append )
-  | Caml _ | Tex _ | Ascii _ | Hol _ | Lem _ | Isa _ | Lex _ | Menhir _ -> raise ThisCannotHappen
+  | Caml _ | Tex _ | Ascii _ | Hol _ | Lem _ | Lean _ | Isa _ | Lex _ | Menhir _ -> raise ThisCannotHappen
 
 (* skip a nonterm or a metavar in a list of elements *)
 let rec skip_nt_mv (es:element list) =

src/context_pp.ml

@@ -101,7 +101,7 @@ let pp_prod_context m xd lookup (hole:nonterm) (target:nontermroot) (r:rule) (p:
   let lhs_pat = Grammar_pp.pp_symterm m xd sie de lhs_st in
   let lhs = 
     ( match m with
-    | Coq _ | Caml _ -> lhs_pat 
+    | Coq _ | Lean _ | Caml _ -> lhs_pat 
     | Isa _ | Hol _ | Lem _ | Twf _ -> lhs_pat ^ " " ^ Grammar_pp.pp_nonterm m xd hole
     | Lex _ | Menhir _ | Tex _ | Ascii _ -> assert false) in
   (* compute the rhs *)
@@ -130,6 +130,12 @@ let pp_rule_context m xd lookup cr : int_func =
 	  ^ ") ("^fake_hole_var^":"^ Grammar_pp.pp_nontermroot_ty m xd cr.cr_hole ^")",
 	  "",
 	  " : " ^ (Grammar_pp.pp_nontermroot_ty m xd cr.cr_target) ^ " :=\n  match "^ctx_var^" with\n")
+    | Lean _ ->
+	((leanTODO "6" ( id 
+	  ^ " ("^ctx_var^":"^ Grammar_pp.pp_nontermroot_ty m xd cr.cr_ntr 
+	  ^ ") ("^fake_hole_var^":"^ Grammar_pp.pp_nontermroot_ty m xd cr.cr_hole ^")")),
+	  "",
+	  " : " ^ (Grammar_pp.pp_nontermroot_ty m xd cr.cr_target) ^ " :=\n  match "^ctx_var^" with\n")
     | Isa _ ->
 	( id ^ " :: \"" 
 	  ^ Grammar_pp.pp_nontermroot_ty m xd cr.cr_ntr ^ " => "