From 8c780e3ed53a93cb03c7210903a0bac3917cdcc5 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 10 Nov 2021 18:04:52 -0500 Subject: [PATCH] quip: add clause in expr_def --- src/base/Proof_quip.ml | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/src/base/Proof_quip.ml b/src/base/Proof_quip.ml index 1cc9e47d..3078359c 100644 --- a/src/base/Proof_quip.ml +++ b/src/base/Proof_quip.ml @@ -170,12 +170,21 @@ end = struct add_needed_step c; add_needed_step rhs; let name = name_clause lid in - let step = lazy ( + (* add [name := (|- c=rhs) by refl c]. + Make sure we do it first, order in final proof will be reversed. *) + let step_refl = lazy ( + let c = L_terms.find c in + let rhs = L_terms.find rhs in + P.S_step_c {name; res=[P.Lit.eq c rhs]; proof=P.refl c} + ) in + add_top_step step_refl; + (* define [c:=rhs] *) + let step_def = lazy ( let c = L_terms.find c in let rhs = L_terms.find rhs in P.S_define_t (c, rhs) ) in - add_top_step step; + add_top_step step_def; L_proofs.add lid (lazy (P.ref_by_name name)); | PS.Step_view.Expr_not { f } ->