From 7b4f197d37a5f1bdf470676f6879c607a45a3477 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 4 Jul 2020 23:58:47 +0200 Subject: Use a dedicated type for equality elimination. In this mess of higher-order callbacks it helps sorting out the invariants of the structure. --- tactics/equality.ml | 32 +++++++++++++++++++++----------- 1 file changed, 21 insertions(+), 11 deletions(-) diff --git a/tactics/equality.ml b/tactics/equality.ml index b4def7bb51..ecc9436db6 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1013,6 +1013,10 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq to_kind = Proofview.tclUNIT (applist (eq_elim, [t;t1;mkNamedLambda (make_annot e Sorts.Relevant) t discriminator;i;t2])) +type equality = { + eq_data : (coq_eq_data * EConstr.t * (EConstr.t * EConstr.t * EConstr.t)); + eq_clenv : clausenv; +} let eq_baseid = Id.of_string "e" @@ -1025,7 +1029,7 @@ let apply_on_clause (f,t) clause = | _ -> user_err (str "Ill-formed clause applicator.")) in clenv_fchain ~with_univs:false argmv f_clause clause -let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = +let discr_positions env sigma { eq_data = (lbeq,eqn,(t,t1,t2)); eq_clenv = eq_clause } cpath dirn = build_coq_True () >>= fun true_0 -> build_coq_False () >>= fun false_0 -> let false_ty = Retyping.get_type_of env sigma false_0 in @@ -1049,7 +1053,8 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = tclTHENS (assert_after Anonymous false_0) [onLastHypId gen_absurdity; (Logic.refiner ~check:true EConstr.Unsafe.(to_constr pf))] -let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = +let discrEq eq = + let { eq_data = (_, _, (_, t1, t2)); eq_clenv = eq_clause } = eq in let sigma = eq_clause.evd in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -1058,7 +1063,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let info = Exninfo.reify () in tclZEROMSG ~info (str"Not a discriminable equality.") | Inl (cpath, (_,dirn), _) -> - discr_positions env sigma u eq_clause cpath dirn + discr_positions env sigma eq cpath dirn end let onEquality with_evars tac (c,lbindc) = @@ -1071,9 +1076,10 @@ let onEquality with_evars tac (c,lbindc) = let eqn = clenv_type eq_clause' in (* FIXME evar leak *) let (eq,u,eq_args) = pf_apply find_this_eq_data_decompose gl eqn in + let eq = { eq_data = (eq,eqn,eq_args); eq_clenv = eq_clause' } in tclTHEN (Proofview.Unsafe.tclEVARS eq_clause'.evd) - (tac (eq,eqn,eq_args) eq_clause') + (tac eq) end let onNegatedEquality with_evars tac = @@ -1385,7 +1391,8 @@ let simplify_args env sigma t = | eq, [t1;c1;t2;c2] -> applist (eq,[t1;simpl env sigma c1;t2;simpl env sigma c2]) | _ -> t -let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = +let inject_at_positions env sigma l2r eq posns tac = + let { eq_data = (eq,_,(t,t1,t2)); eq_clenv = eq_clause } = eq in let e = next_ident_away eq_baseid (vars_of_env env) in let e_env = push_named (LocalAssum (make_annot e Sorts.Relevant,t)) env in let evdref = ref sigma in @@ -1422,7 +1429,8 @@ let () = CErrors.register_handler (function | NothingToInject -> Some (Pp.str "Nothing to inject.") | _ -> None) -let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause = +let injEqThen keep_proofs tac l2r eql = + let { eq_data = (eq,_,(t,t1,t2)); eq_clenv = eq_clause } = eql in let sigma = eq_clause.evd in let env = eq_clause.env in match find_positions env sigma ~keep_proofs ~no_discr:true t1 t2 with @@ -1437,7 +1445,7 @@ let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause = | Inr [([],_,_)] -> Proofview.tclZERO NothingToInject | Inr posns -> - inject_at_positions env sigma l2r u eq_clause posns + inject_at_positions env sigma l2r eql posns (tac (clenv_value eq_clause)) let get_previous_hyp_position id gl = @@ -1491,17 +1499,18 @@ let simpleInjClause flags with_evars = function let injConcl flags = injClause flags None false None let injHyp flags clear_flag id = injClause flags None false (Some (clear_flag,ElimOnIdent CAst.(make id))) -let decompEqThen keep_proofs ntac (lbeq,_,(t,t1,t2) as u) clause = +let decompEqThen keep_proofs ntac eq = + let { eq_data = (_,_,(_,t1,t2) as u); eq_clenv = clause } = eq in Proofview.Goal.enter begin fun gl -> let sigma = clause.evd in let env = Proofview.Goal.env gl in match find_positions env sigma ~keep_proofs ~no_discr:false t1 t2 with | Inl (cpath, (_,dirn), _) -> - discr_positions env sigma u clause cpath dirn + discr_positions env sigma eq cpath dirn | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *) ntac (clenv_value clause) 0 | Inr posns -> - inject_at_positions env sigma true u clause posns + inject_at_positions env sigma true eq posns (ntac (clenv_value clause)) end @@ -1516,7 +1525,8 @@ let dEq ~keep_proofs with_evars = let intro_decomp_eq tac data (c, t) = Proofview.Goal.enter begin fun gl -> let cl = pf_apply make_clenv_binding gl (c, t) NoBindings in - decompEqThen !keep_proof_equalities_for_injection (fun _ -> tac) data cl + let eq = { eq_data = data; eq_clenv = cl } in + decompEqThen !keep_proof_equalities_for_injection (fun _ -> tac) eq end let () = declare_intro_decomp_eq intro_decomp_eq -- cgit v1.2.3 From b1aa5d4583f2c3523b27330f8808f883d0bc8e5a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 5 Jul 2020 00:20:12 +0200 Subject: Do not look for a quantified inductive type in intropattern injection. The code below checks that the term is an applied equality, so allowing non-trivially quantified inductive types would trigger an error right after. --- tactics/tactics.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index eb7b7e363f..3b2481bc69 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2330,7 +2330,7 @@ let intro_decomp_eq ?loc l thin tac id = let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let sigma, t = Typing.type_of env sigma c in - let _,t = reduce_to_quantified_ind env sigma t in + let _,t = reduce_to_atomic_ind env sigma t in match my_find_eq_data_decompose env sigma t with | Some (eq,u,eq_args) -> !intro_decomp_eq_function -- cgit v1.2.3 From 8f484215c8f9beddeffbf0787dbd23265dddfc29 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 5 Jul 2020 00:56:13 +0200 Subject: Remove redundant data from the equality eliminator datatype. --- tactics/equality.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/tactics/equality.ml b/tactics/equality.ml index ecc9436db6..7ad672008e 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1014,7 +1014,7 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq to_kind = (applist (eq_elim, [t;t1;mkNamedLambda (make_annot e Sorts.Relevant) t discriminator;i;t2])) type equality = { - eq_data : (coq_eq_data * EConstr.t * (EConstr.t * EConstr.t * EConstr.t)); + eq_data : (coq_eq_data * (EConstr.t * EConstr.t * EConstr.t)); eq_clenv : clausenv; } @@ -1029,7 +1029,7 @@ let apply_on_clause (f,t) clause = | _ -> user_err (str "Ill-formed clause applicator.")) in clenv_fchain ~with_univs:false argmv f_clause clause -let discr_positions env sigma { eq_data = (lbeq,eqn,(t,t1,t2)); eq_clenv = eq_clause } cpath dirn = +let discr_positions env sigma { eq_data = (lbeq,(t,t1,t2)); eq_clenv = eq_clause } cpath dirn = build_coq_True () >>= fun true_0 -> build_coq_False () >>= fun false_0 -> let false_ty = Retyping.get_type_of env sigma false_0 in @@ -1047,14 +1047,14 @@ let discr_positions env sigma { eq_data = (lbeq,eqn,(t,t1,t2)); eq_clenv = eq_cl in discriminator >>= fun discriminator -> discrimination_pf e (t,t1,t2) discriminator lbeq false_kind >>= fun pf -> - let pf_ty = mkArrow eqn Sorts.Relevant false_0 in + let pf_ty = mkArrow (clenv_type eq_clause) Sorts.Relevant false_0 in let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in let pf = Clenv.clenv_value_cast_meta absurd_clause in tclTHENS (assert_after Anonymous false_0) [onLastHypId gen_absurdity; (Logic.refiner ~check:true EConstr.Unsafe.(to_constr pf))] let discrEq eq = - let { eq_data = (_, _, (_, t1, t2)); eq_clenv = eq_clause } = eq in + let { eq_data = (_, (_, t1, t2)); eq_clenv = eq_clause } = eq in let sigma = eq_clause.evd in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -1076,7 +1076,7 @@ let onEquality with_evars tac (c,lbindc) = let eqn = clenv_type eq_clause' in (* FIXME evar leak *) let (eq,u,eq_args) = pf_apply find_this_eq_data_decompose gl eqn in - let eq = { eq_data = (eq,eqn,eq_args); eq_clenv = eq_clause' } in + let eq = { eq_data = (eq, eq_args); eq_clenv = eq_clause' } in tclTHEN (Proofview.Unsafe.tclEVARS eq_clause'.evd) (tac eq) @@ -1392,7 +1392,7 @@ let simplify_args env sigma t = | _ -> t let inject_at_positions env sigma l2r eq posns tac = - let { eq_data = (eq,_,(t,t1,t2)); eq_clenv = eq_clause } = eq in + let { eq_data = (eq, (t,t1,t2)); eq_clenv = eq_clause } = eq in let e = next_ident_away eq_baseid (vars_of_env env) in let e_env = push_named (LocalAssum (make_annot e Sorts.Relevant,t)) env in let evdref = ref sigma in @@ -1430,7 +1430,7 @@ let () = CErrors.register_handler (function | _ -> None) let injEqThen keep_proofs tac l2r eql = - let { eq_data = (eq,_,(t,t1,t2)); eq_clenv = eq_clause } = eql in + let { eq_data = (eq, (t,t1,t2)); eq_clenv = eq_clause } = eql in let sigma = eq_clause.evd in let env = eq_clause.env in match find_positions env sigma ~keep_proofs ~no_discr:true t1 t2 with @@ -1500,7 +1500,7 @@ let injConcl flags = injClause flags None false None let injHyp flags clear_flag id = injClause flags None false (Some (clear_flag,ElimOnIdent CAst.(make id))) let decompEqThen keep_proofs ntac eq = - let { eq_data = (_,_,(_,t1,t2) as u); eq_clenv = clause } = eq in + let { eq_data = (_, (_,t1,t2) as u); eq_clenv = clause } = eq in Proofview.Goal.enter begin fun gl -> let sigma = clause.evd in let env = Proofview.Goal.env gl in @@ -1522,10 +1522,10 @@ let dEq ~keep_proofs with_evars = dEqThen ~keep_proofs with_evars (fun clear_flag c x -> (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)) -let intro_decomp_eq tac data (c, t) = +let intro_decomp_eq tac (eq, _, data) (c, t) = Proofview.Goal.enter begin fun gl -> let cl = pf_apply make_clenv_binding gl (c, t) NoBindings in - let eq = { eq_data = data; eq_clenv = cl } in + let eq = { eq_data = (eq, data); eq_clenv = cl } in decompEqThen !keep_proof_equalities_for_injection (fun _ -> tac) eq end -- cgit v1.2.3 From 93ac07bbb48ba3a2eca0d5c75aa9be7095a19912 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 2 Sep 2020 18:07:54 +0200 Subject: Document the Equality.equality type in the ML file. --- tactics/equality.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/tactics/equality.ml b/tactics/equality.ml index 7ad672008e..8a406ce8c5 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1015,7 +1015,9 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq to_kind = type equality = { eq_data : (coq_eq_data * (EConstr.t * EConstr.t * EConstr.t)); + (* equality data + A : Type, t1 : A, t2 : A *) eq_clenv : clausenv; + (* clause [M : R A t1 t2] where [R] is the equality from above *) } let eq_baseid = Id.of_string "e" -- cgit v1.2.3