From 90a2644e855a00dc01e3fd7b8a9cf52cc0cc53b6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Tue, 1 Jul 2025 19:48:02 +0200 Subject: [PATCH 01/11] improve applicability of the apply tactic --- src/core/libTerm.ml | 10 +++++++ src/handle/command.ml | 2 +- src/handle/tactic.ml | 66 +++++++++++++++++++++++++++++++------------ 3 files changed, 59 insertions(+), 19 deletions(-) diff --git a/src/core/libTerm.ml b/src/core/libTerm.ml index 861e84f8e..eee54a504 100644 --- a/src/core/libTerm.ml +++ b/src/core/libTerm.ml @@ -202,3 +202,13 @@ let rec free_vars (t:term): VarSet.t = Array.fold_right (fun t acc -> VarSet.union acc (free_vars t)) ts VarSet.empty | _ -> VarSet.empty + +(** [count_products norm a] returns the product arity of the term [a], + reducing codomains with [norm] if needed. *) +let count_products : (ctxt -> term -> term) -> ctxt -> term -> int = + fun norm c -> + let rec count is_norm acc t = + match t with + | Prod(_,b) -> count false (acc + 1) (subst b mk_Kind) + | _ -> if is_norm then acc else count true acc (norm c t) + in count false 0 diff --git a/src/handle/command.ml b/src/handle/command.ml index 3fcf7a204..153dbe24b 100644 --- a/src/handle/command.ml +++ b/src/handle/command.ml @@ -250,7 +250,7 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output = | Prefix _ | Postfix _ | Quant -> 1 | Infix _ -> 2 | _ -> assert false - and real = Tactic.count_products [] !(s.sym_type) in + and real = LibTerm.count_products Eval.whnf [] !(s.sym_type) in if real < expected then fatal pos "Notation incompatible with the type of %a" sym s; (* Check that the notation is compatible with the theory. *) diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index b424cffc5..6c7d15fdb 100644 --- a/src/handle/tactic.ml +++ b/src/handle/tactic.ml @@ -181,15 +181,6 @@ let tac_induction : popt -> proof_state -> goal_typ -> goal list let ids = Ctxt.names ctx in let term = term_in ids in fatal pos "[%a] is not a product." term goal_type -(** [count_products a] returns the number of consecutive products at - the top of the term [a]. *) -let count_products : ctxt -> term -> int = fun c -> - let rec count acc t = - match Eval.whnf c t with - | Prod(_,b) -> count (acc + 1) (subst b mk_Kind) - | _ -> acc - in count 0 - (** [get_prod_ids env do_whnf t] returns the list [v1;..;vn] if [do_whnf] is true and [whnf t] is of the form [Π v1:A1, .., Π vn:An, u] with [u] not a product, or if [do_whnf] is false and [t] is of the form [Π v1:A1, .., Π @@ -455,21 +446,60 @@ let rec handle : | P_tac_solve -> assert false (* done before *) | P_tac_admit -> tac_admit ss sym_pos ps gt | P_tac_apply pt -> + let c = Env.to_ctxt env in let t = scope pt in - (* Compute the product arity of the type of [t]. *) - (* FIXME: this does not take into account implicit arguments. *) - let n = - let c = Env.to_ctxt env in - let p = new_problem () in + let a = + let p = new_problem() in match Infer.infer_noexn p c t with | None -> let ids = Ctxt.names c in let term = term_in ids in fatal pos "[%a] is not typable." term t - | Some (_, a) -> count_products c a + | Some (_, a) -> a in - let t = scope (P.appl_wild pt n) in - let p = new_problem () in - tac_refine pos ps gt gs p t + (* We now try to find [k >= 0] such that [a] reduces to [Π x1:A1, .., Π + xk:Ak, B] and [B] matches [u]. *) + let time = Time.save () in + let rec find u is_whnf k xs a = + if Logger.log_enabled() then log "apply %b %d %a" is_whnf k term a; + Time.restore time; + match Rewrite.matching_subs (xs,a) u with + | Some _ -> Some k + | None -> + match unfold a with + | Prod(_,b) -> + let x,b = unbind b in + find u false (k+1) (Array.append xs [|x|]) b + | _ -> + if is_whnf then None + else + match a with + | Appl(a1,a2) -> + let a2 = unfold a2 and a2' = Eval.whnf [] a2 in + if a2 == a2' then None + else find u true k xs (mk_Appl(a1,a2')) + | _ -> None + in + let r = + match find gt.goal_type false 0 [||] a with + | Some _ as r -> r + | None -> + match gt.goal_type with + | Appl(u1,u2) -> + let u2 = unfold u2 and u2' = Eval.whnf c u2 in + if u2 == u2' then None + else find (mk_Appl(u1,u2')) false 0 [||] a + | _ -> None + in + begin + match r with + | Some k -> + let t = scope (P.appl_wild pt k) in + let p = new_problem () in + tac_refine pos ps gt gs p t + | None -> + fatal pos "Could not find a subterm of [%a] or of its whnf \ + matching the current goal or its whnf." term a + end | P_tac_assume idopts -> (* Check that no idopt is None. *) if List.exists ((=) None) idopts then From dbb6eaa24783284e4fcf2667ec41eec5e038e85f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Wed, 2 Jul 2025 15:17:49 +0200 Subject: [PATCH 02/11] wip --- src/core/eval.ml | 24 ++++++++----- src/core/eval.mli | 7 ++-- src/core/term.ml | 2 +- src/handle/rewrite.ml | 11 +++--- src/handle/tactic.ml | 81 +++++++++++++++++++++++++++++++------------ tests/OK/List.lp | 32 ++++++++--------- tests/OK/Nat.lp | 16 ++++----- 7 files changed, 109 insertions(+), 64 deletions(-) diff --git a/src/core/eval.ml b/src/core/eval.ml index 61061fcbc..9fcebf4f5 100644 --- a/src/core/eval.ml +++ b/src/core/eval.ml @@ -467,29 +467,29 @@ and tree_walk : config -> dtree -> stack -> (term * stack) option = (** {1 Define exposed functions} that take optional arguments rather than a config. *) -type reducer = ?tags:rw_tag list -> ctxt -> term -> term +type 'a reducer = ?tags:rw_tag list -> ctxt -> term -> 'a -let time_reducer (f: reducer): reducer = - let open Stdlib in let r = ref mk_Kind in fun ?tags cfg t -> +let time_reducer (x:'a) (f: 'a reducer): 'a reducer = + let open Stdlib in let r = ref x in fun ?tags cfg t -> Debug.(record_time Rewriting (fun () -> r := f ?tags cfg t)); !r (** [snf ~dtree c t] computes a snf of [t], unfolding the variables defined in the context [c]. The function [dtree] maps symbols to dtrees. *) -let snf : ?dtree:(sym -> dtree) -> reducer = fun ?dtree ?tags c t -> +let snf : ?dtree:(sym -> dtree) -> term reducer = fun ?dtree ?tags c t -> Stdlib.(steps := 0); let u = snf (whnf (Config.make ?dtree ?tags c)) t in if Stdlib.(!steps = 0) then unfold t else u -let snf ?dtree = time_reducer (snf ?dtree) +let snf ?dtree = time_reducer mk_Kind (snf ?dtree) (** [hnf c t] computes a hnf of [t], unfolding the variables defined in the context [c], and using user-defined rewrite rules. *) -let hnf : reducer = fun ?tags c t -> +let hnf : term reducer = fun ?tags c t -> Stdlib.(steps := 0); let u = hnf (whnf (Config.make ?tags c)) t in if Stdlib.(!steps = 0) then unfold t else u -let hnf = time_reducer hnf +let hnf = time_reducer mk_Kind hnf (** [eq_modulo c a b] tests the convertibility of [a] and [b] in context [c]. WARNING: may have side effects in TRef's introduced by whnf. *) @@ -508,12 +508,18 @@ let pure_eq_modulo : ?tags:rw_tag list -> ctxt -> term -> term -> bool = (** [whnf c t] computes a whnf of [t], unfolding the variables defined in the context [c], and using user-defined rewrite rules if [~rewrite]. *) -let whnf : reducer = fun ?tags c t -> +let whnf_opt : term option reducer = fun ?tags c t -> + Stdlib.(steps := 0); + let u = whnf (Config.make ?tags c) t in + if Stdlib.(!steps = 0) then None else Some u + +let whnf : term reducer = fun ?tags c t -> Stdlib.(steps := 0); let u = whnf (Config.make ?tags c) t in if Stdlib.(!steps = 0) then unfold t else u -let whnf = time_reducer whnf +let whnf = time_reducer mk_Kind whnf +let whnf_opt = time_reducer None whnf_opt (** [beta_simplify c t] computes a beta whnf of [t] in context [c] belonging to the set S such that (1) terms of S are in beta whnf normal format, (2) diff --git a/src/core/eval.mli b/src/core/eval.mli index fec870f0d..b36793694 100644 --- a/src/core/eval.mli +++ b/src/core/eval.mli @@ -45,10 +45,13 @@ type rw_tag = (** {b NOTE} that all reduction functions, and {!eq_modulo}, may reduce in-place some subterms of the reduced term. *) -(** [whnf ?tags c t] computes a whnf of the term [t] in context - [c]. *) +(** [whnf ?tags c t] computes a whnf of the term [t] in context [c]. *) val whnf : ?tags:rw_tag list -> ctxt -> term -> term +(** [whnf ?tags c t] returns some whnf of the term [t] in context [c] if it is + different from [t]. *) +val whnf_opt : ?tags:rw_tag list -> ctxt -> term -> term option + (** [eq_modulo c a b] tests the convertibility of [a] and [b] in context [c]. *) val eq_modulo : ?tags:rw_tag list -> ctxt -> term -> term -> bool diff --git a/src/core/term.ml b/src/core/term.ml index 6c9c753a3..af6b08e6d 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -878,7 +878,7 @@ let add_args : term -> term list -> term = fun t ts -> List.fold_left (fun t u -> mk_Appl(t,u)) t ts | _ -> List.fold_left (fun t u -> Appl(t,u)) t ts -(** [add_args_map f t ts] is equivalent to [add_args t (List.map f ts)] but +(** [add_args_map t f ts] is equivalent to [add_args t (List.map f ts)] but more efficient. *) let add_args_map : term -> (term -> term) -> term list -> term = fun t f ts -> match get_args t with diff --git a/src/handle/rewrite.ml b/src/handle/rewrite.ml index 1dd23d51c..1f14fe1b0 100644 --- a/src/handle/rewrite.ml +++ b/src/handle/rewrite.ml @@ -122,7 +122,8 @@ let get_eq_data : let rec get_eq vs t notin_whnf = if Logger.log_enabled () then log "get_eq %a" term t; match get_args t with - | Prod(_,t), _ -> let v,t = unbind t in get_eq (v::vs) t true + | Prod(_,t), _ -> + let v,t = unbind ~name:("$"^binder_name t) t in get_eq (v::vs) t true | p, [u] when is_symb cfg.symb_P p -> begin let u = Eval.whnf ~tags:[`NoRw;`NoExpand] [] u in @@ -161,7 +162,7 @@ let matches : term -> term -> bool = if Term.cmp p t = 0 then eq l else begin let hp, ps, kp = get_args_len p and ht, ts, kt = get_args_len t in if Logger.log_enabled() then - log "matches? %a %a ≡ %a %a" + log "%a %a \nmatches? %a %a" term hp (D.list term) ps term ht (D.list term) ts; match hp with | Wild -> assert false (* used in user syntax only *) @@ -207,15 +208,15 @@ let matches : term -> term -> bool = let r = try eq [p,t]; true with Not_equal -> false in if Logger.log_enabled() then log "matches result: %b" r; r -let no_match ?(subterm=false) pos (*g_env*) (vars,p) t = +let no_match ?(subterm=false) pos (*g_env*) (_vars,p) t = (* Rename [vars] with names distinct from those of [g_env] and [t]. *) (*let f idmap x = let name, idmap = Name.get_safe_prefix (base_name x) idmap in idmap, mk_Vari (new_var name) in let ts = snd (Array.fold_left_map f (Env.names g_env) vars) in*) - let ts = Array.map (fun v -> mk_Vari (new_var ("$"^base_name v))) vars in - let p = msubst (bind_mvar vars p) ts in + (*let ts = Array.map (fun v -> mk_Vari (new_var ("$"^base_name v))) vars in + let p = msubst (bind_mvar vars p) ts in*) if subterm then fatal pos "No subterm of [%a] matches [%a]." term t term p else fatal pos "[%a] doesn't match [%a]." term t term p diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index 6c7d15fdb..f62e597f7 100644 --- a/src/handle/tactic.ml +++ b/src/handle/tactic.ml @@ -446,8 +446,8 @@ let rec handle : | P_tac_solve -> assert false (* done before *) | P_tac_admit -> tac_admit ss sym_pos ps gt | P_tac_apply pt -> - let c = Env.to_ctxt env in let t = scope pt in + let c = Env.to_ctxt env in let a = let p = new_problem() in match Infer.infer_noexn p c t with @@ -458,37 +458,72 @@ let rec handle : in (* We now try to find [k >= 0] such that [a] reduces to [Π x1:A1, .., Π xk:Ak, B] and [B] matches [u]. *) - let time = Time.save () in - let rec find u is_whnf k xs a = - if Logger.log_enabled() then log "apply %b %d %a" is_whnf k term a; - Time.restore time; - match Rewrite.matching_subs (xs,a) u with + let is_reduced = Stdlib.ref false in + let rec ext_whnf c t = + if Logger.log_enabled() then log "ext_whnf %a" term t; + match Eval.whnf_opt c t with + | Some t' -> Stdlib.(is_reduced := true); t' + | None -> + match get_args t with + | (Symb s) as h, ts when is_constant s -> + add_args_map h (ext_whnf c) ts + | _ -> t + in + (*let print_result s f arg x result = + let r = f x in + if Logger.log_enabled() then log "%s %a ≡ %a" s arg x result r; + r + in*) + (*let ext_whnf c t = + print_result "ext_whnf" (ext_whnf c) term t term in*) + let top_ext_whnf c t = + if Logger.log_enabled() then log "top_ext_whnf %a" term t; + match Eval.whnf_opt c t with + | Some t' -> Stdlib.(is_reduced := true); t' + | None -> + match unfold t with + | Appl(pi,u) -> mk_Appl(pi,ext_whnf c u) + | _ -> t + in + (*let top_ext_whnf c t = + print_result "top_ext_whnf" (top_ext_whnf c) term t term in*) + let top_ext_whnf_opt c t = + if Logger.log_enabled() then log "top_ext_whnf_opt %a" term t; + Stdlib.(is_reduced := false); + let t' = top_ext_whnf c t in + if Stdlib.(!is_reduced) then Some t' else None + in + (*let top_ext_whnf_opt c t = + print_result "top_ext_whnf_opt" + (top_ext_whnf_opt c) term t (D.option term) in*) + let rec find goal k xs lem is_whnf_lem = + if Logger.log_enabled() then + log "find %d %a %b\nmatching %a" k term lem is_whnf_lem term goal; + let t0 = Time.save() in + match Rewrite.matching_subs (xs,lem) goal with | Some _ -> Some k | None -> - match unfold a with + Time.restore t0; + match unfold lem with | Prod(_,b) -> - let x,b = unbind b in - find u false (k+1) (Array.append xs [|x|]) b + let x,lem' = unbind ~name:("$"^binder_name b) b in + find goal (k+1) (Array.append xs [|x|]) lem' false | _ -> - if is_whnf then None + if is_whnf_lem then None else - match a with - | Appl(a1,a2) -> - let a2 = unfold a2 and a2' = Eval.whnf [] a2 in - if a2 == a2' then None - else find u true k xs (mk_Appl(a1,a2')) - | _ -> None + match top_ext_whnf_opt [] lem with + | None -> None + | Some lem' -> find goal k xs lem' true in let r = - match find gt.goal_type false 0 [||] a with + let t0 = Time.save () in + match find gt.goal_type 0 [||] a false with | Some _ as r -> r | None -> - match gt.goal_type with - | Appl(u1,u2) -> - let u2 = unfold u2 and u2' = Eval.whnf c u2 in - if u2 == u2' then None - else find (mk_Appl(u1,u2')) false 0 [||] a - | _ -> None + Time.restore t0; + match top_ext_whnf_opt c gt.goal_type with + | None -> None + | Some u -> find u 0 [||] a false in begin match r with diff --git a/tests/OK/List.lp b/tests/OK/List.lp index 4208529e3..d626d3762 100644 --- a/tests/OK/List.lp +++ b/tests/OK/List.lp @@ -225,7 +225,7 @@ end; opaque symbol □≠⸬ [a] [x:τ a] [l] : π (□ ≠ x ⸬ l) ≔ begin - assume a x l h; refine @⸬≠□ a x l _; symmetry; apply h + assume a x l h; apply @⸬≠□ a x l; symmetry; apply h end; // head @@ -246,7 +246,7 @@ with behead (_ ⸬ $l) ↪ $l; opaque symbol ⸬_inj [a] [x:τ a] [l y m] : π(x ⸬ l = y ⸬ m) → π(x = y ∧ l = m) ≔ begin - assume a x l y m e; apply ∧ᵢ { apply feq (head x) e } { apply feq behead e } + assume a x l y m e; apply ∧ᵢ { refine feq (head x) e } { refine feq behead e } end; // boolean equality on lists @@ -270,7 +270,7 @@ begin { simplify; assume c; refine ⊥ₑ c; } { simplify; assume y m i c; apply feq2 (⸬) _ _ - { apply beq_correct; apply @andₑ₁ _ (eql beq l m) c} + { apply beq_correct; apply @andₑ₁ _ (eql beq l m) c } { apply h; refine @andₑ₂ (beq x y) _ c } } @@ -702,7 +702,7 @@ begin { assume i j; apply ⊥ₑ (s≠0 j); } { assume eb lb k; induction { assume m; reflexivity; } - { assume i m n; apply h lb i _; apply +1_inj n; } + { assume i m n; refine h lb i _; apply +1_inj n; } } } end; @@ -748,7 +748,7 @@ begin { assume n h; induction { reflexivity; } - { assume e l i; simplify; refine h l; } + { assume e l i; refine h l; } } end; @@ -926,7 +926,7 @@ begin { reflexivity; } { assume m i; induction { reflexivity; } - { assume e l j; simplify; apply i l; } + { assume e l j; refine i l; } } } end; @@ -1088,7 +1088,7 @@ opaque symbol mem_take [a] beq n l (x:τ a) : begin assume a beq n l x h; rewrite left cat_take_drop n l; rewrite mem_cat beq x (take n l) (drop n l); - refine @orᵢ₁ (∈ beq x (take n l)) (∈ beq x (drop n l)) h; + refine @orᵢ₁ _ (∈ beq x (drop n l)) h; end; opaque symbol mem_drop [a] beq n l (x:τ a) : @@ -1096,7 +1096,7 @@ opaque symbol mem_drop [a] beq n l (x:τ a) : begin assume a beq n l x h; rewrite left cat_take_drop n l; rewrite mem_cat beq x (take n l) (drop n l); - refine @orᵢ₂ (∈ beq x (take n l)) (∈ beq x (drop n l)) h; + refine @orᵢ₂ (∈ beq x (take n l)) _ h; end; opaque symbol mem_rcons_left [a] beq (n m : τ a) (l : 𝕃 a) : @@ -1104,15 +1104,15 @@ opaque symbol mem_rcons_left [a] beq (n m : τ a) (l : 𝕃 a) : begin assume a beq n m; induction - { assume h; refine ⊥ₑ h } + { assume h; apply ⊥ₑ h } { assume n0 l h1 h2; have H0: π (beq n n0) → π (beq n n0 or ∈ beq n (rcons l m)) { assume h3; - refine (orᵢ₁ [beq n n0] (∈ beq n (rcons l m)) h3) }; + refine (orᵢ₁ (∈ beq n (rcons l m)) h3) }; have H1: π (∈ beq n l) → π (beq n n0 or ∈ beq n (rcons l m)) { assume h3; - refine (orᵢ₂ (beq n n0) [∈ beq n (rcons l m)] (h1 h3)) }; - refine orₑ [beq n n0] [∈ beq n l] (beq n n0 or ∈ beq n (rcons l m)) h2 H0 H1 } + refine (orᵢ₂ (beq n n0) (h1 h3)) }; + refine orₑ (beq n n0 or ∈ beq n (rcons l m)) h2 H0 H1 } end; opaque symbol 0∈indexes⸬ [a] (x : τ a) (l: 𝕃 a) : @@ -1135,7 +1135,7 @@ begin { assume k h1 m; simplify; assume h2; refine orₑ [eqn n m] [∈ eqn n (iota (m +1) k)] (eqn n m or ∈ eqn (n +1) (iota ((m +1) +1) k)) h2 _ _ { assume h3; - refine orᵢ₁ [eqn n m] (∈ eqn (n +1) (iota ((m +1) +1) k)) h3 } + refine orᵢ₁ (∈ eqn (n +1) (iota ((m +1) +1) k)) h3 } { assume h3; refine orᵢ₂ (eqn n m) [∈ eqn (n +1) (iota ((m +1) +1) k)] _; refine h1 (m +1) _; refine h3 @@ -1152,8 +1152,8 @@ begin { simplify; assume x h; refine h } { assume x l h y; simplify; assume i; refine orₑ [eqn n 0] [∈ eqn n (iota 1 (size l))] _ i _ _ - { assume j; apply orᵢ₁ [eqn n 0] (∈ eqn (n +1) (iota 2 (size l))) j } - { assume j; apply orᵢ₂ (eqn n 0) [∈ eqn (n +1) (iota 2 (size l))] _; + { assume j; refine orᵢ₁ (∈ eqn (n +1) (iota 2 (size l))) j } + { assume j; refine orᵢ₂ (eqn n 0) [∈ eqn (n +1) (iota 2 (size l))] _; refine +1∈iota+1 n 1 (size l) j; } } @@ -1584,7 +1584,7 @@ begin { assume e1 l1 i; induction { assume j; apply ⊥ₑ (⸬≠□ j) } { - simplify; assume e2 l2 j k; refine feq2 (⸬) _ _ + simplify; assume e2 l2 j k; apply feq2 (⸬) _ _ { apply h; apply ∧ₑ₁ (⸬_inj k) } { apply i; apply ∧ₑ₂ (⸬_inj k) } } diff --git a/tests/OK/Nat.lp b/tests/OK/Nat.lp index 9818d7e7f..68e76d4ef 100644 --- a/tests/OK/Nat.lp +++ b/tests/OK/Nat.lp @@ -133,7 +133,7 @@ with ($x +1) ∸1 ↪ $x; opaque symbol +1_inj [x y] : π (x +1 = y +1) → π (x = y) ≔ begin - assume x y h; apply feq (∸1) h + assume x y h; refine feq (∸1) h end; // boolean equality on ℕ @@ -329,7 +329,7 @@ begin } { assume x h; induction { refine s≠0 } - { assume y i j; apply h y; apply +1_inj; apply +1_inj; apply j } + { assume y i j; apply h y; apply +1_inj; apply +1_inj; refine j } } end; @@ -847,11 +847,11 @@ opaque symbol leq_add2l p m n : π (istrue (p + m ≤ p + n) ⇔ istrue (m ≤ n begin assume p m n; apply ∧ᵢ { generalize p; induction - { assume m n h; apply h } + { assume m n h; refine h } { assume p h m n i; apply h m n i } } { generalize p; induction - { assume m n h; apply h } + { assume m n h; refine h } { assume p h m n i; apply h m n i } }; end; @@ -954,7 +954,7 @@ begin have t: π (istrue (m < n)) { apply h n j }; have u: π (istrue (m +1 < n +1)) { refine ∧ₑ₂ (ltn_add2r (_0 +1) m n) t }; - rewrite left addn1 m; rewrite left addn1 n; apply u; + rewrite left addn1 m; rewrite left addn1 n; refine u; } } } { @@ -983,12 +983,12 @@ begin assume m n p; apply ∧ᵢ { assume h; have t: π (((m - (n + p)) = _0)) → π (istrue (m ≤ (n + p))) - { apply ∧ₑ₁ (subn_eq0 m (n + p)) }; + { refine ∧ₑ₁ (subn_eq0 m (n + p)) }; apply t; rewrite subnDA; apply ∧ₑ₂ (subn_eq0 (m - n) p) h; } { assume h; have t: π (((m - n) - p) = _0) → π (istrue ((m - n) ≤ p)) - { apply ∧ₑ₁ (subn_eq0 (m - n) p) }; + { refine ∧ₑ₁ (subn_eq0 (m - n) p) }; apply t; rewrite left subnDA; apply ∧ₑ₂ (subn_eq0 m (n + p)) h; }; end; @@ -1008,7 +1008,7 @@ begin induction { assume n; apply eq_refl n } { assume m h; induction - { apply eq_refl (m +1) } + { reflexivity } { assume n i; simplify; apply feq (+1); apply h n } } end; From 8eb1eb8c56a9efe4c9e284744c24bf2927f7666e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Wed, 2 Jul 2025 17:20:39 +0200 Subject: [PATCH 03/11] wip --- src/handle/proof.ml | 7 +++---- src/handle/tactic.ml | 4 ++-- 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/src/handle/proof.ml b/src/handle/proof.ml index 4d0ad09c3..eeb66a25c 100644 --- a/src/handle/proof.ml +++ b/src/handle/proof.ml @@ -62,10 +62,9 @@ module Goal = struct let hyps : int StrMap.t -> goal pp = let hyps elt ppf l = if l <> [] then - out ppf "@[%a@,\ - -----------------------------------------------\ - ---------------------------------@,@]" - (List.pp (fun ppf -> out ppf "%a@," elt) "") (List.rev l); + out ppf "%a---------------------------------------------\ + ---------------------------------\n" + (List.pp (fun ppf -> out ppf "%a\n" elt) "") (List.rev l); in fun idmap ppf g -> diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index f62e597f7..67d752108 100644 --- a/src/handle/tactic.ml +++ b/src/handle/tactic.ml @@ -74,7 +74,7 @@ let tac_admit: Sig_state.t -> popt -> proof_state -> goal_typ -> proof_state = (** [tac_solve pos ps] tries to simplify the unification goals of the proof state [ps] and fails if constraints are unsolvable. *) let tac_solve : popt -> proof_state -> proof_state = fun pos ps -> - if Logger.log_enabled () then log "@[tac_solve@ %a@]" goals ps; + if Logger.log_enabled() then log "tac_solve"; (* convert the proof_state into a problem *) let gs_typ, gs_unif = List.partition is_typ ps.proof_goals in let p = new_problem() in @@ -116,7 +116,7 @@ let tac_refine : ?check:bool -> popt -> proof_state -> goal_typ -> goal list -> problem -> term -> proof_state = fun ?(check=true) pos ps gt gs p t -> - if Logger.log_enabled () then log "@[tac_refine@ %a@]" term t; + if Logger.log_enabled () then log "tac_refine %a" term t; let c = Env.to_ctxt gt.goal_hyps in if LibMeta.occurs gt.goal_meta c t then fatal pos "Circular refinement."; (* Check that [t] has the required type. *) From 16d3b1ba1b031bf9131cb3fa6a010ad8fbcd8e08 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Wed, 2 Jul 2025 19:13:35 +0200 Subject: [PATCH 04/11] wip --- src/handle/proof.ml | 2 +- src/handle/tactic.ml | 88 +++++++++++++++++++++++++------------------- 2 files changed, 52 insertions(+), 38 deletions(-) diff --git a/src/handle/proof.ml b/src/handle/proof.ml index eeb66a25c..92918b6b8 100644 --- a/src/handle/proof.ml +++ b/src/handle/proof.ml @@ -126,7 +126,7 @@ let goals : proof_state pp = fun ppf ps -> | g::gs -> let idmap = get_names g in out ppf "%a0. %a@." (Goal.hyps idmap) g (Goal.pp_aux idmap) g; - let goal ppf i g = out ppf "%d. %a@," (i+1) Goal.pp_no_hyp g in + let goal ppf i g = out ppf "%d. %a@." (i+1) Goal.pp_no_hyp g in List.iteri (goal ppf) gs (** [remove_solved_goals ps] removes from the proof state [ps] the typing diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index 67d752108..86e3d418a 100644 --- a/src/handle/tactic.ml +++ b/src/handle/tactic.ml @@ -118,22 +118,21 @@ let tac_refine : ?check:bool -> fun ?(check=true) pos ps gt gs p t -> if Logger.log_enabled () then log "tac_refine %a" term t; let c = Env.to_ctxt gt.goal_hyps in - if LibMeta.occurs gt.goal_meta c t then fatal pos "Circular refinement."; (* Check that [t] has the required type. *) let t = if check then match Infer.check_noexn p c t gt.goal_type with | None -> let ids = Ctxt.names c in let term = term_in ids in - fatal pos "%a@ does not have type@ %a." term t term gt.goal_type + fatal pos "%a\ndoes not have type\n%a." term t term gt.goal_type | Some t -> t else t in + if LibMeta.occurs gt.goal_meta c t then fatal pos "Circular refinement."; if Logger.log_enabled () then log (Color.red "%a ≔ %a") meta gt.goal_meta term t; LibMeta.set p gt.goal_meta (bind_mvar (Env.vars gt.goal_hyps) t); (* Convert the metas and constraints of [p] not in [gs] into new goals. *) - if Logger.log_enabled () then log "%a" problem p; tac_solve pos {ps with proof_goals = Proof.add_goals_of_problem p gs} (** [ind_data t] returns the [ind_data] structure of [s] if [t] is of the @@ -446,19 +445,10 @@ let rec handle : | P_tac_solve -> assert false (* done before *) | P_tac_admit -> tac_admit ss sym_pos ps gt | P_tac_apply pt -> - let t = scope pt in - let c = Env.to_ctxt env in - let a = - let p = new_problem() in - match Infer.infer_noexn p c t with - | None -> - let ids = Ctxt.names c in let term = term_in ids in - fatal pos "[%a] is not typable." term t - | Some (_, a) -> a - in - (* We now try to find [k >= 0] such that [a] reduces to [Π x1:A1, .., Π - xk:Ak, B] and [B] matches [u]. *) let is_reduced = Stdlib.ref false in + (* [ext_whnf] reduces a term to whnf and, if it is already in whnf, + reduce also its subterms similarly. Records also whether there has + been a reduction. *) let rec ext_whnf c t = if Logger.log_enabled() then log "ext_whnf %a" term t; match Eval.whnf_opt c t with @@ -471,11 +461,14 @@ let rec handle : in (*let print_result s f arg x result = let r = f x in - if Logger.log_enabled() then log "%s %a ≡ %a" s arg x result r; - r - in*) + if Logger.log_enabled() then log "%s %a ≡ %a" s arg x result r; + r + in*) (*let ext_whnf c t = print_result "ext_whnf" (ext_whnf c) term t term in*) + (* [top_ext_whnf] reduces a term to whnf and, if it is already in + whnf and of the form [Appl(_,u)], then reduces [u] according to + [ext_whnf]. Records also whether there has been a reduction. *) let top_ext_whnf c t = if Logger.log_enabled() then log "top_ext_whnf %a" term t; match Eval.whnf_opt c t with @@ -496,9 +489,12 @@ let rec handle : (*let top_ext_whnf_opt c t = print_result "top_ext_whnf_opt" (top_ext_whnf_opt c) term t (D.option term) in*) + (* Try to find [k >= 0] such that [lem] reduces to [Π x1:A1, .., Π + xk:Ak, B] and [B] matches [goal]. *) let rec find goal k xs lem is_whnf_lem = if Logger.log_enabled() then - log "find %d %a %b\nmatching %a" k term lem is_whnf_lem term goal; + log "find %d %a %b\nmatching %a" + k term lem is_whnf_lem term goal; let t0 = Time.save() in match Rewrite.matching_subs (xs,lem) goal with | Some _ -> Some k @@ -515,25 +511,43 @@ let rec handle : | None -> None | Some lem' -> find goal k xs lem' true in - let r = - let t0 = Time.save () in - match find gt.goal_type 0 [||] a false with - | Some _ as r -> r - | None -> - Time.restore t0; - match top_ext_whnf_opt c gt.goal_type with - | None -> None - | Some u -> find u 0 [||] a false - in begin - match r with - | Some k -> - let t = scope (P.appl_wild pt k) in - let p = new_problem () in - tac_refine pos ps gt gs p t - | None -> - fatal pos "Could not find a subterm of [%a] or of its whnf \ - matching the current goal or its whnf." term a + let t = scope pt in + let c = Env.to_ctxt env in + if let p = new_problem() in + Infer.check_noexn p c t gt.goal_type <> None + && Unif.solve_noexn p && Timed.(!p).unsolved = [] + then + let p = new_problem() in + tac_refine pos ps gt gs p t + else + let a = + let p = new_problem() in + match Infer.infer_noexn p c t with + | None -> + let ids = Ctxt.names c in + let term = term_in ids in + fatal pos "[%a] is not typable." term t + | Some (_, a) -> a + in + let r = + let t0 = Time.save () in + match find gt.goal_type 0 [||] a false with + | Some _ as r -> r + | None -> + Time.restore t0; + match top_ext_whnf_opt c gt.goal_type with + | None -> None + | Some u -> find u 0 [||] a false + in + match r with + | Some k -> + let t = scope (P.appl_wild pt k) in + let p = new_problem() in + tac_refine pos ps gt gs p t + | None -> + fatal pos "Could not find a subterm of [%a] or of its whnf \ + matching the current goal or its whnf." term a end | P_tac_assume idopts -> (* Check that no idopt is None. *) From c4d903effef08684565bf6bc19a28273061b4755 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Wed, 2 Jul 2025 19:34:28 +0200 Subject: [PATCH 05/11] --- tests/OK/Comp.lp | 87 ++++++ tests/OK/Pos.lp | 584 +++++++++++++++++++++++++++++++++++++++ tests/OK/Z.lp | 697 +++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 1368 insertions(+) create mode 100644 tests/OK/Comp.lp create mode 100644 tests/OK/Pos.lp create mode 100644 tests/OK/Z.lp diff --git a/tests/OK/Comp.lp b/tests/OK/Comp.lp new file mode 100644 index 000000000..0f040868e --- /dev/null +++ b/tests/OK/Comp.lp @@ -0,0 +1,87 @@ +/* Comparison datatype + +By Quentin Garchery (May 2021). */ + +require open tests.OK.Set tests.OK.Prop tests.OK.FOL tests.OK.Eq + tests.OK.Bool; + +inductive Comp : TYPE ≔ +| Eq : Comp +| Lt : Comp +| Gt : Comp; + +// set code for Comp + +constant symbol comp : Set; + +rule τ comp ↪ Comp; + +// Boolean functions for testing head constructor + +symbol isEq : Comp → 𝔹; + +rule isEq Eq ↪ true +with isEq Lt ↪ false +with isEq Gt ↪ false; + +symbol isLt : Comp → 𝔹; + +rule isLt Eq ↪ false +with isLt Lt ↪ true +with isLt Gt ↪ false; + +symbol isGt : Comp → 𝔹; + +rule isGt Eq ↪ false +with isGt Lt ↪ false +with isGt Gt ↪ true; + +symbol isLe : Comp → 𝔹; + +rule isLt Eq ↪ true +with isLt Lt ↪ true +with isLt Gt ↪ false; + +symbol isGe : Comp → 𝔹; + +rule isLt Eq ↪ true +with isLt Lt ↪ false +with isLt Gt ↪ true; + +// Discriminate constructors + +symbol Lt≠Eq : π (Lt ≠ Eq) ≔ +begin + assume h; refine ind_eq h (λ n, istrue(isEq n)) ⊤ᵢ +end; + +symbol Gt≠Eq : π (Gt ≠ Eq) ≔ +begin + assume h; refine ind_eq h (λ n, istrue(isEq n)) ⊤ᵢ +end; + +symbol Gt≠Lt : π (Gt ≠ Lt) ≔ +begin + assume h; refine ind_eq h (λ n, istrue(isLt n)) ⊤ᵢ +end; + +// Opposite of a Comp + +symbol opp : Comp → Comp; + +rule opp Eq ↪ Eq +with opp Lt ↪ Gt +with opp Gt ↪ Lt; + +symbol opp_idem c : π (opp (opp c) = c) ≔ +begin + induction { reflexivity; } { reflexivity; } { reflexivity; } +end; + +// Conditional + +symbol case_Comp [A] : Comp → τ A → τ A → τ A → τ A; + +rule case_Comp Eq $x _ _ ↪ $x +with case_Comp Lt _ $x _ ↪ $x +with case_Comp Gt _ _ $x ↪ $x; diff --git a/tests/OK/Pos.lp b/tests/OK/Pos.lp new file mode 100644 index 000000000..b42d95a44 --- /dev/null +++ b/tests/OK/Pos.lp @@ -0,0 +1,584 @@ +/* Positive binary integers + +by Quentin Garchery (May 2021). */ + +require open tests.OK.Set tests.OK.Prop tests.OK.FOL tests.OK.Eq + tests.OK.Nat tests.OK.Bool tests.OK.Comp; + +inductive ℙ : TYPE ≔ +| I : ℙ → ℙ +| O : ℙ → ℙ +| H : ℙ; + +// set code for ℙ + +constant symbol pos : Set; + +rule τ pos ↪ ℙ; + +// boolean functions for testing head constructor + +symbol isI : ℙ → 𝔹; + +rule isI (I _) ↪ true +with isI (O _) ↪ false +with isI H ↪ false; + +symbol isO : ℙ → 𝔹; + +rule isO (I _) ↪ false +with isO (O _) ↪ true +with isO H ↪ false; + +symbol isH : ℙ → 𝔹; + +rule isH (I _) ↪ false +with isH (O _) ↪ false +with isH H ↪ true; + +// Discriminate constructors + +symbol I≠H [x] : π (I x ≠ H) ≔ +begin + assume x h; refine ind_eq h (λ x, istrue(isH x)) ⊤ᵢ; +end; + +symbol O≠H [x] : π (O x ≠ H) ≔ +begin + assume x h; refine ind_eq h (λ x, istrue(isH x)) ⊤ᵢ; +end; + +symbol I≠O [x y] : π (I x ≠ O y) ≔ +begin + assume x y h; refine ind_eq h (λ x, istrue(isO x)) ⊤ᵢ; +end; + +opaque symbol caseH x : π(x = H ∨ x ≠ H) ≔ +begin + induction + { assume x h; apply ∨ᵢ₂; refine I≠H } + { assume x h; apply ∨ᵢ₂; refine O≠H } + { apply ∨ᵢ₁; reflexivity } +end; + +// Constructors are injective + +symbol projO : ℙ → ℙ; + +rule projO (O $x) ↪ $x +with projO (I $x) ↪ I $x +with projO H ↪ H; + +opaque symbol O_inj p q : π(O p = O q) → π(p = q) ≔ +begin + assume p q h; apply feq projO h +end; + +symbol projI : ℙ → ℙ; + +rule projI (I $x) ↪ $x +with projI (O $x) ↪ O $x +with projI H ↪ H; + +opaque symbol I_inj p q : π(I p = I q) → π(p = q) ≔ +begin + assume p q h; apply feq projI h +end; + +// Successor function + +symbol succ : ℙ → ℙ; + +rule succ (I $x) ↪ O (succ $x) +with succ (O $x) ↪ I $x +with succ H ↪ O H; + +// Interpretation of ℙ in ℕ + +symbol val : ℙ → ℕ; + +rule val H ↪ 1 +with val (O $x) ↪ 2 * val $x +with val (I $x) ↪ val (O $x) +1; + +assert ⊢ val (O (I H)) ≡ 6; + +opaque symbol valS x : π(val (succ x) = val x +1) ≔ +begin + induction + { assume x h; simplify; rewrite h; reflexivity } + { assume x h; reflexivity } + { reflexivity } +end; + +opaque symbol val_surj [n] : π(n ≠ 0 ⇒ `∃ x, val x = n) ≔ +begin + induction + { assume h; apply ⊥ₑ; apply h; reflexivity } + { assume n h i; apply ∨ₑ (casen n) + { assume j; apply ∃ᵢ H; rewrite j; reflexivity } + { assume j; apply ∃ₑ (h j); assume p k; apply ∃ᵢ (succ p); + rewrite left k; apply valS p /*FIXME*/ } + } +end; + +opaque symbol val≠0 x : π(val x ≠ 0) ≔ +begin + induction + { assume x h; refine s≠0 } + { assume x h; simplify; assume i; + apply h (∧ₑ₁ (∧ₑ₁ (addn_eq0 (val x) (val x)) i)) + } + { refine s≠0 } +end; + +opaque symbol 2*val≠0 x : π(val x + val x ≠ 0) ≔ +begin + assume x h; apply ⊥ₑ; apply val≠0 x; apply 2*=0; apply h +end; + +opaque symbol val_inj [x y] : π(val x = val y) → π(x = y) ≔ +begin + induction + { assume x h; induction + { simplify; assume y i j; rewrite h y _ + { apply 2*_inj; apply +1_inj; apply j } + { reflexivity } + } + { simplify; assume y i j; apply ⊥ₑ; apply odd≠even (val x) (val y) j } + { simplify; assume i; apply ⊥ₑ; apply 2*val≠0 x; apply +1_inj; apply i } + } + { assume x h; induction + { simplify; assume y i j; apply ⊥ₑ; + apply odd≠even (val y) (val x) (eq_sym j) } + { simplify; assume y i j; apply feq O; apply h; apply 2*_inj; apply j } + { assume i; apply ⊥ₑ; apply odd≠even 0 (val x); symmetry; apply i } + } + { induction + { simplify; assume x h i; apply ⊥ₑ; apply val≠0 x; apply 2*=0; apply +1_inj; + symmetry; apply i } + { simplify; assume x h i; apply ⊥ₑ; apply odd≠even 0 (val x); apply i } + { reflexivity } + } +end; + +// ℕ-like Induction Principle + +symbol ind_ℙeano p : π (p H) → (Π x, π (p x) → π (p (succ x))) → Π x, π (p x) ≔ +begin + assume p pH psucc; + have i: π(`∀ n, `∀ x, val x = n ⇒ p x) { + induction + { induction + { assume x h i; apply ⊥ₑ (s≠0 i) } + { assume x h i; apply ⊥ₑ (val≠0 (O x) i) } + { assume i; apply ⊥ₑ (s≠0 i) } + } + { assume n h x; apply ∨ₑ (casen n) + { assume i; rewrite i; assume j; + have k: π(x = H) { apply val_inj; apply j }; + rewrite k; apply pH + } + { assume i; apply ∃ₑ (val_surj i); assume y j; rewrite left j; + rewrite left valS; assume k; have l: π(x = succ y) { apply val_inj k }; + rewrite l; apply psucc y; apply h; apply j + } + } + }; + assume x; apply i (val x); reflexivity +end; + +// Addition of ℙ numbers with and without a carry + +symbol add : ℙ → ℙ → ℙ; +symbol add_carry : ℙ → ℙ → ℙ; + +rule add (I $x) (I $q) ↪ O (add_carry $x $q) +with add (I $x) (O $q) ↪ I (add $x $q) +with add (O $x) (I $q) ↪ I (add $x $q) +with add (O $x) (O $q) ↪ O (add $x $q) +with add $x H ↪ succ $x +with add H $y ↪ succ $y; + +rule add_carry (I $x) (I $q) ↪ I (add_carry $x $q) +with add_carry (I $x) (O $q) ↪ O (add_carry $x $q) +with add_carry (O $x) (I $q) ↪ O (add_carry $x $q) +with add_carry (O $x) (O $q) ↪ I (add $x $q) +with add_carry $x H ↪ add $x (O H) +with add_carry H $y ↪ add (O H) $y; +// for efficiency reasons last cases should not be 'succ (succ $x)' + +// Check that 7 + 5 = 12 +assert ⊢ add (I (I H)) (I (O H)) ≡ O (O (I H)); +// Check that 110101010 + 101101100 ≡ 1100010110 in base 2 (426 + 364 ≡ 790) +assert ⊢ add (O (I (O (I (O (I (O (I H)))))))) + (O (O (I (I (O (I (I (O H)))))))) + ≡ (O (I (I (O (I (O (O (O (I H))))))))); + +// Interaction of succ and add + +symbol succ_add x y : π (succ (add x y) = add_carry x y) ≔ +begin + induction + // case I + { assume p prec; + induction + { reflexivity } + { assume q h; simplify; rewrite prec; reflexivity } + { reflexivity } } + // case O + { assume p prec; + induction + { assume q h; simplify; rewrite prec; reflexivity } + { reflexivity } + { reflexivity } } + // case H + { induction { reflexivity } { reflexivity } { reflexivity } } +end; + +symbol add_succ x y : π (add (succ x) y = succ (add x y)) ≔ +begin + induction + // case I + { assume p prec; + induction + { assume q h; simplify; rewrite prec; rewrite succ_add; reflexivity } + { assume q h; simplify; rewrite prec; reflexivity } + { reflexivity } } + // case O + { assume p prec; + induction + { assume q h; simplify; rewrite succ_add; reflexivity } + { reflexivity } + { reflexivity } } + // case H + { induction { reflexivity } { reflexivity } { reflexivity } } +end; + +symbol add_succ_right x y : π (add x (succ y) = succ (add x y)) ≔ +begin + refine ind_ℙeano (λ x, `∀ y, add x (succ y) = succ (add x y)) _ _ + // case H + { reflexivity } + // case succ + { assume x xrec y; + rewrite add_succ; rewrite add_succ; rewrite xrec; reflexivity } +end; + +// Associativity of the addition + +symbol add_assoc x y z : π (add (add x y) z = add x (add y z)) ≔ +begin + refine ind_ℙeano (λ x, `∀ y, `∀ z, add (add x y) z = add x (add y z)) _ _ + // case H + { refine add_succ } + // case succ + { assume x xrec y z; + rewrite add_succ; rewrite add_succ; rewrite add_succ; + rewrite xrec; reflexivity } +end; + +// Commutativity of the addition + +symbol add_com x y : π (add x y = add y x) ≔ +begin + refine ind_ℙeano (λ x, `∀ y, add x y = add y x) _ _ + // case H + { reflexivity } + // case succ + { assume x xrec y; + rewrite add_succ; rewrite add_succ_right; rewrite xrec; reflexivity } +end; + +// function λ x, 2 * x - 1 + +symbol pos_pred_double : ℙ → ℙ; + +rule pos_pred_double (I $x) ↪ I (O $x) +with pos_pred_double (O $x) ↪ I (pos_pred_double $x) +with pos_pred_double H ↪ H; + +symbol pos_pred_double_succ x : π (pos_pred_double (succ x) = I x) ≔ +begin + induction + { assume x xrec; simplify; rewrite xrec; reflexivity } + { reflexivity } + { reflexivity } +end; + +symbol succ_pos_pred_double x : π (succ (pos_pred_double x) = O x) ≔ +begin + induction + { reflexivity } + { assume x xrec; simplify; rewrite xrec; reflexivity } + { reflexivity } +end; + +// Comparison of ℙ numbers + +symbol compare_acc : ℙ → Comp → ℙ → Comp; + +rule compare_acc (I $x) $c (I $q) ↪ compare_acc $x $c $q +with compare_acc (I $x) _ (O $q) ↪ compare_acc $x Gt $q +with compare_acc (I _) _ H ↪ Gt +with compare_acc (O $x) _ (I $q) ↪ compare_acc $x Lt $q +with compare_acc (O $x) $c (O $q) ↪ compare_acc $x $c $q +with compare_acc (O _) _ H ↪ Gt +with compare_acc H _ (I _) ↪ Lt +with compare_acc H _ (O _) ↪ Lt +with compare_acc H $c H ↪ $c; + +symbol compare x y ≔ compare_acc x Eq y; + +// Commutative property of compare + +symbol compare_acc_com x y c : + π (compare_acc y c x = opp (compare_acc x (opp c) y)) ≔ +begin + induction + // case I + { assume x xrec; + induction + { assume y h c; simplify; rewrite xrec; reflexivity } + { assume y h c; simplify; rewrite xrec; reflexivity } + { reflexivity } } + // case O + { assume x xrec; + induction + { assume y h c; simplify; rewrite xrec; reflexivity } + { assume y h c; simplify; rewrite xrec; reflexivity } + { reflexivity } } + // case H + { induction + { reflexivity } + { reflexivity } + { assume c; simplify; rewrite opp_idem; reflexivity } } +end; + +symbol compare_com x y : π (compare y x = opp (compare x y)) ≔ +begin + assume x y; refine compare_acc_com x y Eq; +end; + +// Compare decides the equality + +symbol compare_acc_nEq x y c : π (c ≠ Eq ⇒ compare_acc x c y ≠ Eq) ≔ +begin + induction + // case I + { assume x xrec; + induction + { assume y h c H; refine xrec y c H } + { assume y h c H; refine xrec y Gt _; refine Gt≠Eq } + { assume c h; refine Gt≠Eq } } + // case O + { assume x xrec; + induction + { assume y h c H; refine xrec y Lt _; refine Lt≠Eq } + { assume y h c H; refine xrec y c H } + { assume c h; refine Gt≠Eq } } + // case H + { induction + { assume y h c H; refine Lt≠Eq } + { assume y h c H; refine Lt≠Eq } + { assume c Hc; refine Hc } } +end; + +symbol compare_decides x y : π (compare x y = Eq ⇒ x = y) ≔ +begin + induction + // case I + { assume x xrec; + induction + { assume y h H; rewrite xrec y H; reflexivity } + { assume y h H; apply ⊥ₑ; refine compare_acc_nEq x y Gt _ H; refine Gt≠Eq } + { assume H; apply ⊥ₑ; refine Gt≠Eq H } } + // case O + { assume x xrec; + induction + { assume y h H; apply ⊥ₑ; refine compare_acc_nEq x y Lt _ H; refine Lt≠Eq } + { assume y h H; rewrite xrec y H; reflexivity } + { assume H; apply ⊥ₑ; refine Gt≠Eq H } } + // case H + { induction + { assume y h H; apply ⊥ₑ; refine Lt≠Eq H } + { assume y h H; apply ⊥ₑ; refine Lt≠Eq H } + { reflexivity } } +end; + +// Compare with Gt or Lt + +symbol compare_Lt x y : + π (compare_acc x Lt y = case_Comp (compare x y) Lt Lt Gt) ≔ +begin + induction + // case I + { assume x xrec; + induction + { assume y h; refine xrec y } + { assume y h; simplify; + refine ind_Comp (λ c, compare_acc x Gt y = c ⇒ c = case_Comp c Lt Lt Gt) _ _ _ (compare_acc x Gt y) _ + { assume H; apply ⊥ₑ; refine compare_acc_nEq x y Gt _ H } + { refine Gt≠Eq } + { reflexivity } + { reflexivity } } + { reflexivity; reflexivity } } + // case O + { assume x xrec; + induction + { assume y h; simplify; + refine ind_Comp (λ c, compare_acc x Lt y = c ⇒ c = case_Comp c Lt Lt Gt) _ _ _ (compare_acc x Lt y) _ + { assume H; apply ⊥ₑ; refine compare_acc_nEq x y Lt _ H } + { refine Lt≠Eq } + { reflexivity } + { reflexivity } } + { reflexivity } + { assume y h; refine xrec y; + reflexivity } } + // case H + { induction { reflexivity } { reflexivity } { reflexivity } } +end; + +symbol compare_Gt x y : + π (compare_acc x Gt y = case_Comp (compare x y) Gt Lt Gt) ≔ +begin + induction + // case I + { assume x xrec; + induction + { assume y h; refine xrec y } + { assume y h; simplify; + refine ind_Comp (λ c, compare_acc x Gt y = c ⇒ c = case_Comp c Gt Lt Gt) _ _ _ (compare_acc x Gt y) _ + { assume H; apply ⊥ₑ; refine compare_acc_nEq x y Gt _ H } + { refine Gt≠Eq } + { reflexivity } + { reflexivity } } + { reflexivity; reflexivity } } + // case O + { assume x xrec; + induction + { assume y h; simplify; + refine ind_Comp (λ c, compare_acc x Lt y = c ⇒ c = case_Comp c Gt Lt Gt) _ _ _ (compare_acc x Lt y) _ + { assume H; apply ⊥ₑ; refine compare_acc_nEq x y Lt _ H } + { refine Lt≠Eq } + { reflexivity } + { reflexivity } } + { reflexivity; assume y h; refine xrec y } + { reflexivity } } + // case H + { induction { reflexivity } { reflexivity } { reflexivity } } +end; + +// Compatibility of compare with the addition + +symbol compare_H_Lt y : π (compare_acc H Lt y = Lt) ≔ +begin + induction { reflexivity } { reflexivity } { reflexivity } +end; + +symbol compare_Gt_H x : π (compare_acc x Gt H = Gt) ≔ +begin + induction { reflexivity } { reflexivity } { reflexivity } +end; + +symbol compare_H_succ y c : π (compare_acc H c (succ y) = Lt) ≔ +begin + induction { reflexivity } { reflexivity } { reflexivity } +end; + +symbol compare_succ_H x c : π (compare_acc (succ x) c H = Gt) ≔ +begin + induction { reflexivity } { reflexivity } { reflexivity } +end; + +symbol compare_succ_Lt x y : + π (compare_acc (succ x) Lt y = compare_acc x Gt y) ≔ +begin + induction + // case I + { assume x xrec; + induction + { assume y h; refine xrec y } + { assume y h; refine xrec y } + { reflexivity } } + // case O + { assume x xrec; + induction { reflexivity } { reflexivity } { reflexivity } } + // case H + { induction + { assume y h; refine compare_H_Lt y } + { assume y h; refine compare_H_Lt y } + { reflexivity } } +end; + +symbol compare_Gt_succ x y : + π (compare_acc x Gt (succ y) = compare_acc x Lt y) ≔ +begin + assume x y; + rewrite compare_acc_com; rewrite .[u in _ = u] compare_acc_com; + simplify; rewrite compare_succ_Lt; reflexivity; +end; + +symbol compare_succ_succ x y c : + π (compare_acc (succ x) c (succ y) = compare_acc x c y) ≔ +begin + induction + // case I + { assume x xrec; + induction + { assume y h c; refine xrec y c } + { assume y h c; simplify; refine compare_succ_Lt x y } + { assume c; simplify; refine compare_succ_H x c } } + // case O + { assume x xrec; + induction + { assume y h c; simplify; refine compare_Gt_succ x y } + { assume y h c; reflexivity } + { assume c; simplify; refine compare_Gt_H x } } + // case H + { induction + { assume y h c; simplify; refine compare_H_succ y c } + { assume y h c; simplify; refine compare_H_Lt y } + { reflexivity } } +end; + +symbol compare_compat_add a x y : + π (compare (add x a) (add y a) = compare x y) ≔ +begin + refine ind_ℙeano (λ a, `∀ x, `∀ y, compare (add x a) (add y a) = compare x y) _ _ + // case H + { assume x y; refine compare_succ_succ x y Eq } + // case succ + { assume a arec x y; + rewrite add_succ_right; rewrite add_succ_right; rewrite left arec x y; + simplify; rewrite compare_succ_succ; reflexivity } +end; + +// Multiplication + +symbol mul : ℙ → ℙ → ℙ; + +rule mul (I $x) $y ↪ add $x (O (mul $x $y)) +with mul (O $x) $y ↪ O (mul $x $y) +with mul H $y ↪ $y; + +// shortcuts + +symbol _1 ≔ H; +symbol _2 ≔ O H; +symbol _3 ≔ I H; +symbol _4 ≔ O (O H); +symbol _5 ≔ I (O H); +symbol _6 ≔ O (I H); +symbol _7 ≔ I (I H); +symbol _8 ≔ O (O (O H)); +symbol _9 ≔ I (O (O H)); +symbol _10 ≔ O (I (O H)); + +// enable printing of natural numbers in decimal notation + +builtin "pos_one" ≔ H; +builtin "pos_double" ≔ O; +builtin "pos_succ_double" ≔ I; + +compute add _2 _2; diff --git a/tests/OK/Z.lp b/tests/OK/Z.lp new file mode 100644 index 000000000..9d7ee1abd --- /dev/null +++ b/tests/OK/Z.lp @@ -0,0 +1,697 @@ +/* Binary integers + +by Quentin Garchery (May 2021). */ + +require open tests.OK.Set tests.OK.Prop tests.OK.FOL tests.OK.Eq tests.OK.Pos tests.OK.Bool; + +inductive ℤ : TYPE ≔ // \BbbZ +| Z0 : ℤ +| Zpos : ℙ → ℤ +| Zneg : ℙ → ℤ; + +// set code for ℤ + +constant symbol int : Set; + +rule τ int ↪ ℤ; + +// boolean functions for testing head constructor + +symbol isZ0 : ℤ → 𝔹; + +rule isZ0 Z0 ↪ true +with isZ0 (Zpos _) ↪ false +with isZ0 (Zneg _) ↪ false; + +symbol isZpos : ℤ → 𝔹; + +rule isZpos Z0 ↪ false +with isZpos (Zpos _) ↪ true +with isZpos (Zneg _) ↪ false; + +symbol isZneg : ℤ → 𝔹; + +rule isZneg Z0 ↪ false +with isZneg (Zpos _) ↪ false +with isZneg (Zneg _) ↪ true; + +// Discriminate constructors + +symbol Zpos≠Z0 p : π (Zpos p ≠ Z0) ≔ +begin + assume n h; refine ind_eq h (λ n, istrue(isZ0 n)) ⊤ᵢ +end; + +symbol Zneg≠Z0 p : π (Zneg p ≠ Z0) ≔ +begin + assume n h; refine ind_eq h (λ n, istrue(isZ0 n)) ⊤ᵢ +end; + +symbol Zpos≠Zneg p q : π (Zpos p ≠ Zneg q) ≔ +begin + assume x y h; refine ind_eq h (λ n, istrue(isZneg n)) ⊤ᵢ +end; + +// Unary opposite + +symbol — : ℤ → ℤ; +notation — prefix 24; + +rule — Z0 ↪ Z0 +with — (Zpos $p) ↪ Zneg $p +with — (Zneg $p) ↪ Zpos $p; + +symbol —_idem z : π (— — z = z) ≔ +begin + induction { reflexivity } { reflexivity } { reflexivity } +end; + +// Doubling functions + +symbol double : ℤ → ℤ; + +rule double Z0 ↪ Z0 +with double (Zpos $p) ↪ Zpos (O $p) +with double (Zneg $p) ↪ Zneg (O $p); + +symbol succ_double : ℤ → ℤ; + +rule succ_double Z0 ↪ Zpos H +with succ_double (Zpos $p) ↪ Zpos (I $p) +with succ_double (Zneg $p) ↪ Zneg (pos_pred_double $p); + +symbol pred_double : ℤ → ℤ; + +rule pred_double Z0 ↪ Zneg H +with pred_double (Zpos $p) ↪ Zpos (pos_pred_double $p) +with pred_double (Zneg $p) ↪ Zneg (I $p); + +// Interaction of opp and doubling functions + +symbol double_opp z : π (double (— z) = — double z) ≔ +begin + induction { reflexivity } { reflexivity } { reflexivity } +end; + +symbol succ_double_opp z : π (succ_double (— z) = — pred_double z) ≔ +begin + induction { reflexivity } { reflexivity } { reflexivity } +end; + +symbol pred_double_opp z : π (pred_double (— z) = — succ_double z) ≔ +begin + induction { reflexivity } { reflexivity } { reflexivity } +end; + +// Binary negation on ℙ + +symbol sub : ℙ → ℙ → ℤ; + +rule sub (I $p) (I $q) ↪ double (sub $p $q) +with sub (I $p) (O $q) ↪ succ_double (sub $p $q) +with sub (I $p) H ↪ Zpos (O $p) +with sub (O $p) (I $q) ↪ pred_double (sub $p $q) +with sub (O $p) (O $q) ↪ double (sub $p $q) +with sub (O $p) H ↪ Zpos (pos_pred_double $p) +with sub H (I $q) ↪ Zneg (O $q) +with sub H (O $q) ↪ Zneg (pos_pred_double $q) +with sub H H ↪ Z0; + +symbol sub_same z : π (sub z z = Z0) ≔ +begin + induction + { assume x xrec; simplify; rewrite xrec; reflexivity } + { assume x xrec; simplify; rewrite xrec; reflexivity } + { reflexivity } +end; + +symbol sub_opp x y : π (— sub x y = sub y x) ≔ +begin + induction + // case I + { assume x xrec; + induction + { assume y h; simplify; rewrite left xrec y; rewrite double_opp; reflexivity } + { assume y h; simplify; rewrite left xrec y; rewrite pred_double_opp; reflexivity } + { reflexivity } } + // case O + { assume x xrec; + induction + { assume y h; simplify; rewrite left xrec y; rewrite succ_double_opp; reflexivity } + { assume y h; simplify; rewrite left xrec y; rewrite double_opp; reflexivity } + { reflexivity } } + // case H + { induction { reflexivity } { reflexivity } { reflexivity } } +end; + +// Addition of integers + +symbol + : ℤ → ℤ → ℤ; +notation + infix right 20; + +rule Z0 + $y ↪ $y +with $x + Z0 ↪ $x +with Zpos $x + Zpos $y ↪ Zpos (add $x $y) +with Zpos $x + Zneg $y ↪ sub $x $y +with Zneg $x + Zpos $y ↪ sub $y $x +with Zneg $x + Zneg $y ↪ Zneg (add $x $y); + +// Interaction of addition with opposite + +symbol distr_—_+ x y : π (— (x + y) = — x + — y) ≔ +begin + induction + // case Z0 + { reflexivity } + // case Zpos + { assume x; + induction + { reflexivity } + { reflexivity } + { assume y; simplify; rewrite sub_opp; reflexivity } } + // case Zneg + { assume x; + induction + { reflexivity } + { assume y; simplify; rewrite sub_opp; reflexivity } + { reflexivity } } +end; + +// Commutativity of addition + +symbol +_com x y : π (x + y = y + x) ≔ +begin + induction + // case Z0 + { induction { reflexivity } { reflexivity } { reflexivity } } + // case Zpos + { assume x; + induction + { reflexivity } + { assume y; simplify; rewrite add_com; reflexivity } + { reflexivity } } + // case Zneg + { assume x; + induction + { reflexivity } + { reflexivity } + { assume y; simplify; rewrite add_com; reflexivity } } +end; + +// Interaction of succ and doubling functions + +symbol pred_double_succ x : π (pred_double (x + Zpos H) = succ_double x) ≔ +begin + induction + { reflexivity } + { assume x; simplify; rewrite pos_pred_double_succ; reflexivity } + { induction { reflexivity } { reflexivity } { reflexivity } } +end; + +symbol succ_pred_double x : π (pred_double x + Zpos H = double x) ≔ +begin + induction + { reflexivity } + { assume x; simplify; rewrite succ_pos_pred_double; reflexivity } + { reflexivity } +end; + +symbol succ_double_carac x : π (succ_double x = double x + Zpos H) ≔ +begin + induction { reflexivity } { reflexivity } { reflexivity } +end; + +symbol double_succ x : π (double (x + Zpos H) = succ_double x + Zpos H) ≔ +begin + induction + { reflexivity } + { reflexivity } + { induction { reflexivity } { reflexivity } { reflexivity } } +end; + +// Negation + +symbol - x y ≔ x + — y; + +notation - infix left 20; + +symbol -_same z : π (z + — z = Z0) ≔ +begin + induction + { reflexivity } + { simplify; refine sub_same } + { simplify; refine sub_same } +end; + +// Associativity + +symbol sub_succ x y : π (sub (succ x) y = sub x y + Zpos H) ≔ +begin + induction + // case I + { assume x xrec; + induction + { assume y h; simplify; rewrite xrec; rewrite pred_double_succ; + rewrite succ_double_carac; reflexivity } + { assume y h; simplify; rewrite xrec; rewrite double_succ; reflexivity } + { simplify; rewrite pos_pred_double_succ; reflexivity } } + // case O + { assume x xrec; + induction + { assume y h; simplify; rewrite left succ_pred_double; reflexivity } + { assume y h; simplify; rewrite succ_double_carac; reflexivity } + { simplify; rewrite succ_pos_pred_double; reflexivity } } + // case H + { induction + { induction { reflexivity } { reflexivity } { reflexivity } } + { induction { reflexivity } { reflexivity } { reflexivity } } + { reflexivity } } +end; + +symbol add_Zpos_succ x p : π (x + Zpos (succ p) = (x + Zpos p) + Zpos H) ≔ +begin + induction + { reflexivity } + { assume x p; simplify; rewrite add_succ_right; reflexivity } + { assume x p; simplify; rewrite sub_succ; reflexivity } +end; + +symbol sub_add_Zpos a b c : π (sub a b + Zpos c = sub (add a c) b) ≔ +begin + assume a b c; + refine ind_ℙeano (λ c, sub a b + Zpos c = sub (add a c) b) _ _ c + // case H + { simplify; rewrite sub_succ; reflexivity } + // case succ + { assume r rrec; rewrite add_Zpos_succ; rewrite rrec; + rewrite add_succ_right; rewrite sub_succ; reflexivity } +end; + +symbol sub_add_Zneg a b c : π (sub a b + Zneg c = sub a (add b c)) ≔ +begin + assume a b c; + rewrite left sub_opp (add b c) a; + rewrite left sub_add_Zpos; + rewrite distr_—_+; rewrite sub_opp; reflexivity; +end; + +symbol +_assoc x y z : π ((x + y) + z = x + (y + z)) ≔ +begin + induction + { reflexivity } + { assume x; + induction + { reflexivity } + { assume y; + induction + { reflexivity } + // case Zpos - Zpos - Zpos + { assume z; simplify; rewrite add_assoc; reflexivity } + // case Zpos - Zpos - Zneg + { assume z; simplify; rewrite +_com; rewrite sub_add_Zpos; + rewrite add_com; reflexivity } } + + { assume y; + induction + { reflexivity } + // case Zpos - Zneg - Zpos + { assume z; simplify; rewrite sub_add_Zpos; rewrite +_com; + rewrite sub_add_Zpos; rewrite add_com; reflexivity } + // case Zpos - Zneg - Zneg + { assume z; simplify; rewrite sub_add_Zneg; reflexivity } } } + + { assume x; + induction + { reflexivity } + { assume y; + induction + { reflexivity } + // case Zneg - Zpos - Zpos + { assume z; simplify; rewrite sub_add_Zpos; reflexivity } + // case Zneg - Zpos - Zneg + { assume z; simplify; rewrite sub_add_Zneg; rewrite +_com; + rewrite sub_add_Zneg; rewrite add_com; reflexivity } } + + { assume y; + induction + { reflexivity } + // case Zneg - Zneg - Zpos + { assume z; simplify; rewrite +_com; rewrite sub_add_Zneg; + rewrite add_com; reflexivity } + // case Zneg - Zneg - Zneg + { assume z; simplify; rewrite add_assoc; reflexivity } } } +end; + +// Comparison of integers + +require open tests.OK.Comp; + +symbol ≐ : ℤ → ℤ → Comp; notation ≐ infix 12; // \doteq + +rule Z0 ≐ Z0 ↪ Eq +with Z0 ≐ Zpos _ ↪ Lt +with Z0 ≐ Zneg _ ↪ Gt +with Zpos _ ≐ Z0 ↪ Gt +with Zpos $p ≐ Zpos $q ↪ compare $p $q +with Zpos _ ≐ Zneg _ ↪ Gt +with Zneg _ ≐ Z0 ↪ Lt +with Zneg _ ≐ Zpos _ ↪ Lt +with Zneg $p ≐ Zneg $q ↪ compare $q $p; + +// ≐ decides the equality of integers + +symbol ≐_decides x y : π (x ≐ y = Eq ⇒ x = y) ≔ +begin + induction + // case Z0 + { induction + { reflexivity } + { assume y H; apply ⊥ₑ; refine Lt≠Eq H } + { assume y H; apply ⊥ₑ; refine Gt≠Eq H } } + // case Zpos + { assume x; + induction + { assume H; apply ⊥ₑ; refine Gt≠Eq H } + { assume y H; rewrite compare_decides x y H; reflexivity } + { assume y H; apply ⊥ₑ; refine Gt≠Eq H } } + // case Zneg + { assume x; + induction + { assume H; apply ⊥ₑ; refine Lt≠Eq H } + { assume y H; apply ⊥ₑ; refine Lt≠Eq H } + { assume y H; rewrite compare_decides y x H; reflexivity } } +end; + +// Commutative properties of ≐ + +symbol ≐_com x y : π (x ≐ y = opp (y ≐ x)) ≔ +begin + induction + // case Z0 + { induction { reflexivity } { reflexivity } { reflexivity } } + // case Zpos + { assume x; + induction + { reflexivity } + { assume y; simplify; rewrite compare_acc_com; reflexivity } + { reflexivity } } + // case Zneg + { assume x; + induction + { reflexivity } + { reflexivity } + { assume y; simplify; rewrite compare_acc_com; reflexivity } } +end; + +symbol ≐_opp x y : π (— x ≐ — y = opp (x ≐ y)) ≔ +begin + induction + // case Z0 + { induction { reflexivity } { reflexivity } { reflexivity } } + // case Zpos + { assume x; + induction + { reflexivity } + { assume y; simplify; rewrite compare_acc_com; reflexivity } + { reflexivity } } + // case Zneg + { assume x; + induction + { reflexivity } + { reflexivity } + { assume y; simplify; rewrite compare_acc_com; reflexivity } } +end; + +// General results + +symbol simpl_right x a : π ((x + a) - a = x) ≔ +begin + assume x a; simplify; rewrite +_assoc; + rewrite -_same; reflexivity; +end; + +symbol simpl_inv_right x a : π ((x - a) + a = x) ≔ +begin + assume x a; simplify; rewrite +_assoc; + rewrite .[— a + a] +_com; rewrite -_same; reflexivity; +end; + +// ≐ with 0 + +symbol ≐_double x : π ((double x ≐ Z0) = (x ≐ Z0)) ≔ +begin + induction { reflexivity } { reflexivity } { reflexivity } +end; + +symbol ≐_pred_double x : + π (pred_double x ≐ Z0 = case_Comp (x ≐ Z0) Lt Lt Gt) ≔ +begin + induction { reflexivity } { reflexivity } { reflexivity } +end; + +symbol ≐_succ_double x : + π (succ_double x ≐ Z0 = case_Comp (x ≐ Z0) Gt Lt Gt) ≔ +begin + induction { reflexivity } { reflexivity } { reflexivity } +end; + +symbol ≐_pos_sub x y : π ((sub x y ≐ Z0) = compare x y) ≔ +begin + induction + // case I + { assume x xrec; + induction + { assume y h; simplify; rewrite ≐_double; refine xrec y } + { assume y h; simplify; rewrite ≐_succ_double; rewrite xrec; + rewrite compare_Gt; reflexivity } + { reflexivity } } + // case O + { assume x xrec; + induction + { assume y h; simplify; rewrite ≐_pred_double; rewrite xrec; + rewrite compare_Lt; reflexivity } + { assume y h; simplify; rewrite ≐_double; refine xrec y } + { reflexivity } } + // case H + { induction { reflexivity } { reflexivity } { reflexivity } } +end; + +symbol ≐_sub x y : π ((x ≐ y) = (x + — y ≐ Z0)) ≔ +begin + induction + // case Z0 + { induction { reflexivity } { reflexivity } { reflexivity } } + // case Zpos + { assume x; + induction + { reflexivity } + { assume y; simplify; rewrite ≐_pos_sub; reflexivity } + { reflexivity } } + // case Zneg + { assume x; + induction + { reflexivity } + { reflexivity } + { assume y; simplify; rewrite ≐_pos_sub; reflexivity } } +end; + +// Compatibility of comparison with the addition + +symbol ≐_compat_add x y z : π ((x ≐ y) = (x + z ≐ y + z)) ≔ +begin + assume x y z; + rewrite ≐_sub; rewrite .[x in _ = x] ≐_sub; + simplify; rewrite distr_—_+; rewrite .[— y + — z] +_com; + rewrite +_assoc; rewrite left +_assoc z (— z) (— y); + rewrite -_same z; reflexivity; +end; + +// Directional comparison operators + +symbol ≤ x y ≔ ¬ (istrue(isGt(x ≐ y))); +notation ≤ infix 10; + +symbol < x y ≔ istrue(isLt(x ≐ y)); +notation < infix 10; + +symbol ≥ x y ≔ ¬ (x < y); +notation ≥ infix 10; + +symbol > x y ≔ ¬ (x ≤ y); +notation > infix 10; + +symbol <_≤ x y : π (x < y ⇒ x ≤ y) ≔ +begin + assume x y; + refine ind_Comp (λ u, istrue(isLt u) ⇒ istrue(isGt u) ⇒ ⊥) _ _ _ (x ≐ y) + { refine (λ x _, x) } + { refine (λ _ y, y) } + { refine (λ x _, x) } +end; + +// Compatibility of directional comparison operators + +symbol ≤_compat_add x y a : π (x ≤ y ⇒ x + a ≤ y + a) ≔ +begin + assume x y a; simplify; + assume H; refine fold_⇒ _; rewrite ≐_sub; + simplify; refine fold_⇒ _; rewrite +_assoc; + rewrite .[y + a] +_com; rewrite distr_—_+; + rewrite left +_assoc a (— a) (— y); rewrite -_same; + rewrite left +_assoc x Z0 (— y); simplify; refine fold_⇒ _; + rewrite left ≐_sub x y; refine H; +end; + +symbol <_compat_add x y a : π (x < y ⇒ x + a < y + a) ≔ +begin + assume x y a; simplify; assume H; rewrite ≐_sub; + simplify; rewrite +_assoc; rewrite .[y + a] +_com; + rewrite distr_—_+; rewrite left +_assoc a (— a) (— y); + rewrite -_same; rewrite left +_assoc; + simplify; rewrite left ≐_sub; refine H; +end; + +symbol ≤_compat_≤ x y : π (Z0 ≤ x ⇒ Z0 ≤ y ⇒ Z0 ≤ x + y) ≔ +begin + induction + { assume y h H; refine H } + { assume x; + induction + { assume h1 h2; refine λ x, x; } + { assume y h h'; refine λ x, x } + { simplify; assume y h f; refine ⊥ₑ _; refine f ⊤ᵢ } } + { assume x y f h; apply ⊥ₑ; refine f ⊤ᵢ } +end; + +symbol <_compat_≤ x y : π (Z0 < x ⇒ Z0 ≤ y ⇒ Z0 < x + y) ≔ +begin + induction + { assume y f h; apply ⊥ₑ; refine f } + { assume x; + induction + { assume h1 h2; refine ⊤ᵢ } + { assume y h h'; refine ⊤ᵢ } + { simplify; assume y h f; apply ⊥ₑ; refine f ⊤ᵢ } } + { assume x; assume y f h; apply ⊥ₑ; refine f } +end; + +// Reflexivity + +symbol ≤_refl x : π (x ≤ x) ≔ +begin + assume x; refine ≤_compat_add Z0 Z0 x _; refine (λ x, x); +end; + +// Antisymmetry + +symbol ≤_antisym x y : π (x ≤ y ⇒ y ≤ x ⇒ x = y) ≔ +begin + assume x y; + have e : π (¬ (istrue(isGt (x ≐ y))) ⇒ ¬ (istrue(isGt (y ≐ x))) ⇒ x = y) + { rewrite ≐_com } ; + refine ind_Comp (λ c, (y ≐ x) = c ⇒ ¬ (istrue(isGt (opp c))) ⇒ ¬ (istrue(isGt c)) ⇒ x = y) _ _ _ (y ≐ x) _ + { assume H h1 h2; symmetry; refine ≐_decides y x H } + { assume h1 f h2; apply ⊥ₑ; refine f ⊤ᵢ } + { assume h1 h2 f; apply ⊥ₑ; refine f ⊤ᵢ } + { reflexivity; refine e } +end; + +// Transitivity theorems + +symbol ≤_trans x y z : π (x ≤ y ⇒ y ≤ z ⇒ x ≤ z) ≔ +begin + assume x y z lxy lyz; + have H : π (Z0 ≤ (z + — y) + (y + — x)) + { refine ≤_compat_≤ (z - y) (y - x) _ _ + { rewrite left -_same y; refine ≤_compat_add y z (— y) _; refine lyz } + { rewrite left -_same x; refine ≤_compat_add x y (— x) _; refine lxy } } ; + generalize H; refine fold_⇒ _; + rewrite +_assoc; rewrite left +_assoc (— y) y (— x); + rewrite .[— y + y] +_com; rewrite -_same; + refine (λ p : π ((Z0 ≤ (z + — x)) ⇒ (x ≤ z)), p) _; + rewrite left .[in x ≤ z] simpl_inv_right z x; + refine ≤_compat_add Z0 (z - x) x; +end; + +symbol <_trans_1 x y z : π (x < y ⇒ y ≤ z ⇒ x < z) ≔ +begin + assume x y z lxy lyz; + have H : π (Z0 < (z + — y) + (y + — x)) + { rewrite +_com; apply <_compat_≤ (y - x) (z - y) + { rewrite left -_same x; refine <_compat_add x y (— x) _; refine lxy } + { rewrite left -_same y; refine ≤_compat_add y z (— y) _; refine lyz } } ; + generalize H; refine fold_⇒ _; + rewrite +_assoc; rewrite left +_assoc (— y) y (— x); + rewrite .[— y + y] +_com; rewrite -_same; + rewrite left .[in x < z] simpl_inv_right z x; + refine <_compat_add Z0 (z - x) x; +end; + +symbol <_trans_2 x y z : π (x ≤ y ⇒ y < z ⇒ x < z) ≔ +begin + assume x y z lxy lyz; + have H : π (Z0 < (z + — y) + (y + — x)) + { apply <_compat_≤ (z - y) (y - x) + { rewrite left -_same y; refine <_compat_add y z (— y) _; refine lyz } + { rewrite left -_same x; refine ≤_compat_add x y (— x) _; refine lxy } }; + generalize H; refine fold_⇒ _; + rewrite +_assoc; rewrite left +_assoc (— y) y (— x); + rewrite .[— y + y] +_com; rewrite -_same; + rewrite left .[in x < z] simpl_inv_right z x; + refine <_compat_add Z0 (z - x) x; +end; + +// Multiplication + +symbol * : ℤ → ℤ → ℤ; +notation * infix right 22; + +rule Z0 * _ ↪ Z0 +with _ * Z0 ↪ Z0 +with Zpos $x * Zpos $y ↪ Zpos (mul $x $y) +with Zpos $x * Zneg $y ↪ Zneg (mul $x $y) +with Zneg $x * Zpos $y ↪ Zneg (mul $x $y) +with Zneg $x * Zneg $y ↪ Zpos (mul $x $y); + +// TO BE CONTINUED (theorems about multiplication) + +// shortcuts + +symbol _1 ≔ Zpos _1; +symbol _2 ≔ Zpos _2; +symbol _3 ≔ Zpos _3; +symbol _4 ≔ Zpos _4; +symbol _5 ≔ Zpos _5; +symbol _6 ≔ Zpos _6; +symbol _7 ≔ Zpos _7; +symbol _8 ≔ Zpos _8; +symbol _9 ≔ Zpos _9; +symbol _10 ≔ Zpos _10; + +// enable printing of integers in decimal notation + +builtin "int_zero" ≔ Z0; +builtin "int_positive" ≔ Zpos; +builtin "int_negative" ≔ Zneg; + +compute _2 - _3; + +// enable parsing of integers in decimal notation + +builtin "0" ≔ Z0; +builtin "1" ≔ _1; +builtin "2" ≔ _2; +builtin "3" ≔ _3; +builtin "4" ≔ _4; +builtin "5" ≔ _5; +builtin "6" ≔ _6; +builtin "7" ≔ _7; +builtin "8" ≔ _8; +builtin "9" ≔ _9; +builtin "10" ≔ _10; + +builtin "+" ≔ +; +builtin "*" ≔ *; +builtin "-" ≔ —; + +type -42; From 12377421b50a07bf5413388591c4cb1c761a4252 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Wed, 2 Jul 2025 19:54:11 +0200 Subject: [PATCH 06/11] wip --- src/handle/tactic.ml | 3 ++- tests/export_raw_dk.sh | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index 86e3d418a..ca915d629 100644 --- a/src/handle/tactic.ml +++ b/src/handle/tactic.ml @@ -547,7 +547,8 @@ let rec handle : tac_refine pos ps gt gs p t | None -> fatal pos "Could not find a subterm of [%a] or of its whnf \ - matching the current goal or its whnf." term a + matching the current goal or its whnf. \ + Try refine instead." term a end | P_tac_assume idopts -> (* Check that no idopt is None. *) diff --git a/tests/export_raw_dk.sh b/tests/export_raw_dk.sh index 26c8e2d3d..059bfaa28 100755 --- a/tests/export_raw_dk.sh +++ b/tests/export_raw_dk.sh @@ -60,7 +60,7 @@ do # proofs why3*|tutorial|try|tautologies|rewrite*|remove|natproofs|have|generalize|foo|comment_in_qid|apply|anonymous|admit);; # "open" - triangular|power-fact|postfix|perf_rw_*|not-eager|nonLeftLinear2|natural|Nat|lpparse2|logic|List|FOL|Eq|doc|Bool|arity_var|arity_diff|922|262_pair_ex_2|215|1141|Tactic|Option|String|HOL|Impred|PropExt|Classic|1217|1151);; + triangular|power-fact|postfix|perf_rw_*|not-eager|nonLeftLinear2|natural|Nat|lpparse2|logic|List|FOL|Eq|doc|Bool|arity_var|arity_diff|922|262_pair_ex_2|215|1141|Tactic|Option|String|HOL|Impred|PropExt|Classic|Comp|Pos|Z|1217|1151);; # "inductive" strictly_positive_*|inductive|989|904|830|341);; # underscore in query From e47ba92afff18137b281bd6fbd750e40673ed461 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Wed, 2 Jul 2025 20:00:42 +0200 Subject: [PATCH 07/11] wip --- .github/workflows/main.yml | 23 ++++++++++++++++------- Makefile | 3 ++- 2 files changed, 18 insertions(+), 8 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index c2585bca8..82c420054 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -16,26 +16,35 @@ jobs: ocaml-version: [5.3.0, 5.2.1, 5.1.1, 5.0.0, 4.14.2, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1] runs-on: ubuntu-latest steps: - - name: checking out lambdapi repo ... + - name: checking out lambdapi repo uses: actions/checkout@v4 - # - name: recovering cached opam files ... + # - name: recovering cached opam files # uses: actions/cache@v4 # with: # path: ~/.opam # key: ${{ runner.os }}-ocaml-${{ matrix.ocaml-version }} - - name: setting up opam ... + - name: setting up opam uses: ocaml/setup-ocaml@v3 with: ocaml-compiler: ${{ matrix.ocaml-version }} - - name: installing dependencies ... + - name: install dependencies run: | opam update opam upgrade opam pin add -n -k path lambdapi . opam install --deps-only -d -t lambdapi - - name: running tests ... + #why3 config detect + - name: sanity_check + run: make sanity_check + - name: run: | - make sanity_check eval $(opam env) - #why3 config detect make tests + - name: + run: | + eval $(opam env) + make tests_export + - name: + run: | + eval $(opam env) + make test_libs diff --git a/Makefile b/Makefile index 897c7de43..4db9fcdd2 100644 --- a/Makefile +++ b/Makefile @@ -34,10 +34,11 @@ tests: lambdapi @dune runtest @tests/runtests.sh @tests/dtrees.sh + +tests_export: lambdapi @tests/export_dk.sh @tests/export_lp.sh @tests/export_raw_dk.sh - $(MAKE) test_libs .PHONY: tests_alt_ergo tests_alt_ergo: lambdapi From 97419950227900dbba6525e8a5ae5706cc151da4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 3 Jul 2025 11:17:05 +0200 Subject: [PATCH 08/11] wip --- .github/workflows/main.yml | 24 +++++++++++++++++------- 1 file changed, 17 insertions(+), 7 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 82c420054..f8a70e393 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -13,7 +13,17 @@ jobs: strategy: fail-fast: false matrix: - ocaml-version: [5.3.0, 5.2.1, 5.1.1, 5.0.0, 4.14.2, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1] + # 5.3.0: 08/01/2025 + # 5.2.1: 18/11/2024 + # 5.1.1: 08/12/2023 + # 5.0.0: 16/12/2022 + # 4.14.2: 15/03/2024 + # 4.13.1: 01/10/2021 + # 4.12.1: 24/02/2021 + # 4.11.2: 24/02/2021 + # 4.10.2: 18/12/2020 + # 4.09.1: 16/03/2020 + ocaml-version: [5.3.0, 5.2.1, 4.14.2] #5.1.1, 5.0.0, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1 runs-on: ubuntu-latest steps: - name: checking out lambdapi repo @@ -29,22 +39,22 @@ jobs: ocaml-compiler: ${{ matrix.ocaml-version }} - name: install dependencies run: | - opam update - opam upgrade + #opam update + #opam upgrade opam pin add -n -k path lambdapi . opam install --deps-only -d -t lambdapi #why3 config detect - - name: sanity_check + - name: make sanity_check run: make sanity_check - - name: + - name: make tests run: | eval $(opam env) make tests - - name: + - name: make tests_export run: | eval $(opam env) make tests_export - - name: + - name: make test_libs run: | eval $(opam env) make test_libs From 525b2e8e82389e4409685ab491c9feb84cda7878 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 4 Jul 2025 10:18:15 +0200 Subject: [PATCH 09/11] wip --- src/core/infer.ml | 2 +- src/core/print.ml | 2 ++ src/core/unif.ml | 65 ++++++++++++++++++++++++++------------------ src/core/unif.mli | 15 +++++----- src/handle/query.ml | 3 +- src/handle/tactic.ml | 2 +- src/lsp/lp_lsp.ml | 6 ++-- 7 files changed, 54 insertions(+), 41 deletions(-) diff --git a/src/core/infer.ml b/src/core/infer.ml index f93619708..66bd6ba0e 100644 --- a/src/core/infer.ml +++ b/src/core/infer.ml @@ -80,7 +80,7 @@ let rec reduce_coercions : ctxt -> term -> term option = fun c t -> [c] and problem [pb]. *) let rec coerce : problem -> ctxt -> term -> term -> term -> term * bool = fun pb c t a b -> - if Logger.log_enabled () then log "coerce %a\n\nto %a" term a term b; + if Logger.log_enabled () then log "coerce %a\nto %a" term a term b; if Eval.pure_eq_modulo c a b then (t, false) else match reduce_coercions c (Coercion.apply a b t) with diff --git a/src/core/print.ml b/src/core/print.ml index b547b3128..acbd36d6b 100644 --- a/src/core/print.ml +++ b/src/core/print.ml @@ -380,6 +380,8 @@ let rec prod_in : int StrMap.t -> (term * bool list) pp = let prod = prod_in StrMap.empty +let sym_type ppf s = prod ppf (!(s.sym_type), s.sym_impl) + let sym_rule : sym_rule pp = fun ppf r -> out ppf "%a ↪ %a" term (lhs r) term (rhs r) diff --git a/src/core/unif.ml b/src/core/unif.ml index afb3ba691..da057eba5 100644 --- a/src/core/unif.ml +++ b/src/core/unif.ml @@ -11,6 +11,24 @@ open Print let log = Logger.make 'u' "unif" "unification" let log = log.pp +(** To indicate whether error messages should be generated. *) +let print_error = Stdlib.ref true + +(** Exception raised when a constraint is not solvable. *) +exception Unsolvable + +(** [error t1 t2] +@raise Unsolvable. *) +let error : ctxt -> term -> term -> 'a = fun c t1 t2 -> + if Stdlib.(!print_error) then + begin + let ids = Ctxt.names c in + let term = term_in ids in + fatal_msg "\n%a\nis not unifiable with\n%a.\n" term t1 term t2 + end; + if Logger.log_enabled() then log "Unsolvable"; + raise Unsolvable + (** Given a meta [m] of type [Πx1:a1,..,Πxn:an,b], [set_to_prod p m] sets [m] to a product term of the form [Πy:m1[x1;..;xn],m2[x1;..;xn;y]] with [m1] and [m2] fresh metavariables, and adds these metavariables to [p]. *) @@ -58,8 +76,7 @@ let add_constr : problem -> constr -> unit = fun p c -> (** [try_unif_rules p c s t] tries to simplify the unification problem [c ⊢ s ≡ t] with the user-defined unification rules. *) -let try_unif_rules : problem -> ctxt -> term -> term -> bool = - fun p c s t -> +let try_unif_rules : problem -> ctxt -> term -> term -> bool = fun p c s t -> if Logger.log_enabled () then log "check unif_rules"; let exception No_match in let open Unif_rule in @@ -77,16 +94,19 @@ let try_unif_rules : problem -> ctxt -> term -> term -> bool = match Infer.infer_noexn p c t, Infer.infer_noexn p c u with | Some (t, a), Some(u, b) -> add_constr p (c,t,u); add_constr p (c,a,b); (c,t,u) - | t', u' -> - (* Error reporting *) - Error.fatal_msg "@[A unification rule generated the \ + | t', u' -> (* Error reporting *) + if Stdlib.(!print_error) then + begin + fatal_msg "@[A unification rule generated the \ ill-typed unification problem@ [%a].@]" - Print.constr (c, t, u); - if t' = None then - Error.fatal_msg "@[Term@ [%a]@ is not typable.@]" term t; - if u' = None then - Error.fatal_msg "@[Term@ [%a]@ is not typable.@]" term u; - Error.fatal_no_pos "Untypable unification problem." + Print.constr (c, t, u); + if t' = None then + fatal_msg "@[Term@ [%a]@ is not typable.@]" term t; + if u' = None then + fatal_msg "@[Term@ [%a]@ is not typable.@]" term u; + fatal_msg "Untypable unification problem." + end; + raise Unsolvable in let cs = List.map (fun (t,u) -> sanitise (c,t,u)) (unpack rhs) in if Logger.log_enabled () then log "rewrites to: %a" constrs cs; @@ -304,17 +324,6 @@ let inverse_opt : sym -> term list -> term -> (term * term) option = | _ -> raise Not_found with Not_found -> if Logger.log_enabled () then log "failed"; None -(** Exception raised when a constraint is not solvable. *) -exception Unsolvable - -(** [error t1 t2] -@raise Unsolvable. *) -let error : ctxt -> term -> term -> 'a = fun c t1 t2 -> - let ids = Ctxt.names c in let term = term_in ids in - fatal_msg "@[%a and %a are not unifiable.@]@." - (D.bracket term) t1 (D.bracket term) t2; - raise Unsolvable - (** [inverse p c t1 s ts1 t2] tries to replace a problem of the form [t1 ≡ t2] with [t1 = s(ts1)] and [ts1=[u]] by [u ≡ inverse s t2], when [s] is injective. *) @@ -502,13 +511,17 @@ let solve : problem -> unit = fun p -> contain constraints that could not be simplified. Metavariable instantiations are type-checked only if the optional argument [~type_check] is [true] (default). *) -let solve_noexn : ?type_check:bool -> problem -> bool = - fun ?(type_check=true) p -> +let solve_noexn : ?print:bool -> ?type_check:bool -> problem -> bool = + fun ?(print=true) ?(type_check=true) p -> Stdlib.(do_type_check := type_check); + Stdlib.(print_error := print); if Logger.log_enabled () then log_hndl (Color.blu "solve_noexn %a") problem p; try time_of "solve" (fun () -> solve p; true) with Unsolvable -> false let solve_noexn = - let open Stdlib in let r = ref false in fun ?type_check p -> - Debug.(record_time Solving (fun () -> r := solve_noexn ?type_check p)); !r + let open Stdlib in + let r = ref false in + fun ?print ?type_check p -> + Debug.(record_time Solving + (fun () -> r := solve_noexn ?print ?type_check p)); !r diff --git a/src/core/unif.mli b/src/core/unif.mli index b2384a1e6..463692ae6 100644 --- a/src/core/unif.mli +++ b/src/core/unif.mli @@ -2,10 +2,11 @@ open Term -(** [solve_noexn ~type_check p] tries to simplify the constraints of [p]. It - returns [false] if it finds a constraint that cannot be - satisfied. Otherwise, [p.to_solve] is empty but [p.unsolved] may still - contain constraints that could not be simplified. Metavariable - instantiations are type-checked only if [~type_check] is [true]. If - [~type_check] is not specified, it defaults to [true]. *) -val solve_noexn : ?type_check:bool -> problem -> bool +(** [solve_noexn ~print ~type_check p] tries to simplify the constraints of + [p]. It returns [false] if it finds a constraint that cannot be + satisfied. Otherwise, [p.to_solve] is empty but [p.unsolved] may still + contain constraints that could not be simplified. Metavariable + instantiations are type-checked only if [~type_check] is [true] + (default). Error messages are generated only if [~print] is [true] + (default). *) +val solve_noexn : ?print:bool -> ?type_check:bool -> problem -> bool diff --git a/src/handle/query.ml b/src/handle/query.ml index b07dc77c7..8463000c7 100644 --- a/src/handle/query.ml +++ b/src/handle/query.ml @@ -132,8 +132,7 @@ let handle : Sig_state.t -> proof_state option -> p_query -> result = let decl ppf s = out ppf "%a%a%asymbol %a : %a%a;@.%a%a" expo s.sym_expo prop s.sym_prop - match_strat s.sym_mstrat sym s - prod (!(s.sym_type), s.sym_impl) + match_strat s.sym_mstrat sym s sym_type s def !(s.sym_def) notation s rules s in (* Function to print constructors and the induction principle if [qid] diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index ca915d629..aabde6cad 100644 --- a/src/handle/tactic.ml +++ b/src/handle/tactic.ml @@ -516,7 +516,7 @@ let rec handle : let c = Env.to_ctxt env in if let p = new_problem() in Infer.check_noexn p c t gt.goal_type <> None - && Unif.solve_noexn p && Timed.(!p).unsolved = [] + && Unif.solve_noexn ~print:false p && Timed.(!p).unsolved = [] then let p = new_problem() in tac_refine pos ps gt gs p t diff --git a/src/lsp/lp_lsp.ml b/src/lsp/lp_lsp.ml index 07567a58a..2dedd34f4 100644 --- a/src/lsp/lp_lsp.ml +++ b/src/lsp/lp_lsp.ml @@ -442,13 +442,11 @@ let hover_symInfo ofmt ~id params = LIO.log_error "symbol map" map_pp; let sym_found = - let open Timed in - let open Term in match StrMap.find_opt sym_target sym with | None -> msg_fail "hover_SymInfo" "Sym not found" - | Some sym -> !(sym.sym_type) + | Some sym -> sym in - let sym_type = Format.asprintf "%a" Core.Print.term sym_found in + let sym_type = Format.asprintf "%a" Core.Print.sym_type sym_found in let result : J.t = `Assoc [ "contents", `String sym_type; "range", range ] in let msg = LSP.mk_reply ~id ~result in From 187b1dd9ecd64df81e4b24c9c119652191103770 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Tue, 15 Jul 2025 17:04:16 +0200 Subject: [PATCH 10/11] fix tests/OK/Comp.lp --- tests/OK/Comp.lp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/tests/OK/Comp.lp b/tests/OK/Comp.lp index 0f040868e..34a1a1e79 100644 --- a/tests/OK/Comp.lp +++ b/tests/OK/Comp.lp @@ -38,15 +38,15 @@ with isGt Gt ↪ true; symbol isLe : Comp → 𝔹; -rule isLt Eq ↪ true -with isLt Lt ↪ true -with isLt Gt ↪ false; +rule isLe Eq ↪ true +with isLe Lt ↪ true +with isLe Gt ↪ false; symbol isGe : Comp → 𝔹; -rule isLt Eq ↪ true -with isLt Lt ↪ false -with isLt Gt ↪ true; +rule isGe Eq ↪ true +with isGe Lt ↪ false +with isGe Gt ↪ true; // Discriminate constructors From 91a0d14bf996a9702917c7dd0c82141fc12668e6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Tue, 15 Jul 2025 18:03:59 +0200 Subject: [PATCH 11/11] wip --- src/core/libTerm.ml | 2 +- src/handle/rewrite.ml | 21 ++++++++------------- src/handle/tactic.ml | 13 +++++++------ tests/OK/Z.lp | 8 ++++---- 4 files changed, 20 insertions(+), 24 deletions(-) diff --git a/src/core/libTerm.ml b/src/core/libTerm.ml index 8ad9280d4..023811db2 100644 --- a/src/core/libTerm.ml +++ b/src/core/libTerm.ml @@ -208,7 +208,7 @@ let rec free_vars (t:term): VarSet.t = let count_products : (ctxt -> term -> term) -> ctxt -> term -> int = fun norm c -> let rec count is_norm acc t = - match t with + match unfold t with | Prod(_,b) -> count false (acc + 1) (subst b mk_Kind) | _ -> if is_norm then acc else count true acc (norm c t) in count false 0 diff --git a/src/handle/rewrite.ml b/src/handle/rewrite.ml index 1f14fe1b0..4492791bb 100644 --- a/src/handle/rewrite.ml +++ b/src/handle/rewrite.ml @@ -123,6 +123,9 @@ let get_eq_data : if Logger.log_enabled () then log "get_eq %a" term t; match get_args t with | Prod(_,t), _ -> + (* We prefix variable names by "$" to distinguish them from the + variables occurring in other assumptions or in the goal, and + because we will try to match them with some subterm of the goal. *) let v,t = unbind ~name:("$"^binder_name t) t in get_eq (v::vs) t true | p, [u] when is_symb cfg.symb_P p -> begin @@ -208,15 +211,7 @@ let matches : term -> term -> bool = let r = try eq [p,t]; true with Not_equal -> false in if Logger.log_enabled() then log "matches result: %b" r; r -let no_match ?(subterm=false) pos (*g_env*) (_vars,p) t = - (* Rename [vars] with names distinct from those of [g_env] and [t]. *) - (*let f idmap x = - let name, idmap = Name.get_safe_prefix (base_name x) idmap in - idmap, mk_Vari (new_var name) - in - let ts = snd (Array.fold_left_map f (Env.names g_env) vars) in*) - (*let ts = Array.map (fun v -> mk_Vari (new_var ("$"^base_name v))) vars in - let p = msubst (bind_mvar vars p) ts in*) +let no_match ?(subterm=false) pos p t = if subterm then fatal pos "No subterm of [%a] matches [%a]." term t term p else fatal pos "[%a] doesn't match [%a]." term t term p @@ -249,10 +244,10 @@ let check_subs pos vars ts = in Array.iteri f ts -let matching_subs_check_TRef pos ((vars,_) as xsp) t = +let matching_subs_check_TRef pos ((vars,p) as xsp) t = match matching_subs xsp t with | Some ts -> check_subs pos vars ts; ts - | None -> no_match pos xsp t + | None -> no_match pos p t (** [find_subst (xs,p) t] tries to find the first instance of a subterm of [t] matching [p]. If successful, the function returns the array of terms by @@ -285,7 +280,7 @@ let find_subst : to_subst -> term -> term array option = fun xsp t -> let find_subst pos (vars,p) t = match find_subst (vars,p) t with - | None -> no_match ~subterm:true pos (vars,p) t + | None -> no_match ~subterm:true pos p t | Some ts -> check_subs pos vars ts; ts (** [find_subterm_matching p t] tries to find a subterm of [t] that matches @@ -325,7 +320,7 @@ let rec replace_wild_by_tref : term -> term = fun t -> let find_subterm_matching pos p t = let p_refs = replace_wild_by_tref p in if not (find_subterm_matching p_refs t) then - no_match ~subterm:true pos ([||],p) t; + no_match ~subterm:true pos p t; p_refs (** [bind_pattern p t] replaces in the term [t] every occurence of the pattern diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index 2795b9e5f..566172767 100644 --- a/src/handle/tactic.ml +++ b/src/handle/tactic.ml @@ -450,9 +450,9 @@ let rec handle : | P_tac_admit -> tac_admit ss sym_pos ps gt | P_tac_apply pt -> let is_reduced = Stdlib.ref false in - (* [ext_whnf] reduces a term to whnf and, if it is already in whnf, - reduce also its subterms similarly. Records also whether there has - been a reduction. *) + (* If [t] is not in whnf, then [ext_whnf t] returns its whnf. Otherwise, + if it is headed by a constant symbol, then it reduces its subterms + similarly. It also records whether there has been a reduction. *) let rec ext_whnf c t = if Logger.log_enabled() then log "ext_whnf %a" term t; match Eval.whnf_opt c t with @@ -470,9 +470,10 @@ let rec handle : in*) (*let ext_whnf c t = print_result "ext_whnf" (ext_whnf c) term t term in*) - (* [top_ext_whnf] reduces a term to whnf and, if it is already in - whnf and of the form [Appl(_,u)], then reduces [u] according to - [ext_whnf]. Records also whether there has been a reduction. *) + (* If [t] is not in whnf, then [top_ext_whnf] returns its + whnf. Otherwise, if [t] is of the form [Appl(_,u)], then it reduces + [u] with [ext_whnf]. It also records whether there has been a + reduction. *) let top_ext_whnf c t = if Logger.log_enabled() then log "top_ext_whnf %a" term t; match Eval.whnf_opt c t with diff --git a/tests/OK/Z.lp b/tests/OK/Z.lp index 9d7ee1abd..e6b8ac057 100644 --- a/tests/OK/Z.lp +++ b/tests/OK/Z.lp @@ -557,10 +557,10 @@ begin { assume y h H; refine H } { assume x; induction - { assume h1 h2; refine λ x, x; } - { assume y h h'; refine λ x, x } - { simplify; assume y h f; refine ⊥ₑ _; refine f ⊤ᵢ } } - { assume x y f h; apply ⊥ₑ; refine f ⊤ᵢ } + { assume h1 h2; refine h1 } + { assume y h h' i; refine i } + { assume y h f h'; refine f ⊤ᵢ } } + { assume x y f h i; refine f ⊤ᵢ } end; symbol <_compat_≤ x y : π (Z0 < x ⇒ Z0 ≤ y ⇒ Z0 < x + y) ≔