diff --git a/hott/types/W.hlean b/hott/types/W.hlean index fc7b6e65d..5dcdf3bdc 100644 --- a/hott/types/W.hlean +++ b/hott/types/W.hlean @@ -109,7 +109,8 @@ namespace Wtype (∀ (b : B a) (b' : B a'), P (f b) (f' b')) → P (sup a f) (sup a' f')) : P w w' := begin revert w', - eapply (Wtype.rec_on w), intro a f IH w', + induction w with a f IH, + intro w', cases w' with a' f', apply H, intro b b', apply IH diff --git a/hott/types/hprop_trunc.hlean b/hott/types/hprop_trunc.hlean index eed5360bf..61baedd17 100644 --- a/hott/types/hprop_trunc.hlean +++ b/hott/types/hprop_trunc.hlean @@ -40,14 +40,14 @@ namespace is_trunc definition is_hprop_is_trunc [instance] (n : trunc_index) : Π (A : Type), is_hprop (is_trunc n A) := begin - eapply (trunc_index.rec_on n), + induction n, { intro A, apply is_trunc_is_equiv_closed, { apply equiv.to_is_equiv, apply is_contr.sigma_char}, apply (@is_hprop.mk), intros, fapply sigma_eq, {apply x.2}, apply (@is_hprop.elim)}, - { intro n' IH A, + { intro A, apply is_trunc_is_equiv_closed, apply equiv.to_is_equiv, apply is_trunc.pi_char}, diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp index cdc11fab4..d178bbef8 100644 --- a/src/library/tactic/induction_tactic.cpp +++ b/src/library/tactic/induction_tactic.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "kernel/abstract.h" +#include "kernel/instantiate.h" #include "kernel/inductive/inductive.h" #include "library/util.h" #include "library/user_recursors.h" @@ -46,7 +47,8 @@ class induction_tac { - non_deps : hypotheses that do not depend on H nor its indices - deps : hypotheses that depend on H or its indices (directly or indirectly) */ - void split_deps(buffer const & hyps, expr const & h, buffer const & indices, buffer & non_deps, buffer & deps) { + void split_deps(buffer const & hyps, expr const & h, buffer const & indices, + buffer & non_deps, buffer & deps) { for (expr const & hyp : hyps) { if (hyp == h) { // we clear h @@ -61,42 +63,22 @@ class induction_tac { } } - bool validate_rec_info(goal const & g, expr const & h, expr const & h_type, recursor_info const & rec_info) { - unsigned nindices = rec_info.get_num_indices(); - if (nindices == 0) - return true; - buffer args; - get_app_args(h_type, args); - if (rec_info.get_num_params() + nindices != args.size()) - return false; - unsigned fidx = args.size() - nindices; - for (unsigned i = fidx; i < args.size(); i++) { - if (!is_local(args[i])) - return false; // the indices must be local constants - for (unsigned j = 0; j < i; j++) { - if (is_local(args[j]) && mlocal_name(args[j]) == mlocal_name(args[i])) - return false; // the indices must be distinct local constants - } - } - if (!rec_info.has_dep_elim() && depends_on(g.get_type(), h)) - return false; - return true; + void throw_ill_formed_recursor(recursor_info const & rec_info) { + throw tactic_exception(sstream() << "invalid 'induction' tactic, recursor '" << rec_info.get_name() + << "' is ill-formed"); } - goals apply_recursor(goal const & g, expr const & h, expr const & h_type, recursor_info const & rec_info) { + goals apply_recursor(goal const & g, unsigned num_deps, expr const & h, expr const & h_type, + buffer const & params, buffer const & indices, + recursor_info const & rec_info) { expr const & g_type = g.get_type(); level g_lvl = sort_level(m_tc.ensure_type(g_type).first); - buffer I_args; - expr const & I = get_app_args(h_type, I_args); - buffer params; - params.append(rec_info.get_num_params(), I_args.data()); - buffer indices; - indices.append(rec_info.get_num_indices(), I_args.data() + params.size()); levels rec_levels; + expr const & I = get_app_fn(h_type); if (auto lpos = rec_info.get_motive_univ_pos()) { buffer ls; unsigned i = 0; - for (level const & l : ls) { + for (level const & l : const_levels(I)) { if (i == *lpos) ls.push_back(g_lvl); ls.push_back(l); @@ -112,32 +94,124 @@ class induction_tac { } rec_levels = const_levels(I); } - expr rec = mk_constant(rec_info.get_name(), rec_levels); - rec = mk_app(rec, params); + expr rec = mk_constant(rec_info.get_name(), rec_levels); + rec = mk_app(rec, params); expr motive = g_type; if (rec_info.has_dep_elim()) motive = Fun(h, motive); motive = Fun(indices, motive); rec = mk_app(rec, motive); - - // TODO(Leo): - regular(m_env, m_ios) << ">> rec: " << rec << "\n"; - - return goals(); + buffer hyps; + g.get_hyps(hyps); + buffer new_hyps; + for (expr const & curr_h : hyps) { + if (mlocal_name(curr_h) != mlocal_name(h) && + std::all_of(indices.begin(), indices.end(), + [&](expr const & idx) { return mlocal_name(curr_h) != mlocal_name(idx); })) { + new_hyps.push_back(curr_h); + } + } + expr rec_type = m_tc.whnf(m_tc.infer(rec).first).first; + unsigned curr_pos = params.size() + 1 /* motive */; + unsigned first_idx_pos = rec_info.get_first_index_pos(); + bool consumed_major = false; + buffer new_goals; + while (is_pi(rec_type) && curr_pos < rec_info.get_num_args()) { + if (first_idx_pos == curr_pos) { + for (expr const & idx : indices) { + rec = mk_app(rec, idx); + rec_type = m_tc.whnf(instantiate(binding_body(rec_type), idx)).first; + if (!is_pi(rec_type)) + throw_ill_formed_recursor(rec_info); + curr_pos++; + } + rec = mk_app(rec, h); + rec_type = m_tc.whnf(instantiate(binding_body(rec_type), h)).first; + consumed_major = true; + curr_pos++; + } else { + buffer new_goal_hyps; + new_goal_hyps.append(new_hyps); + expr new_type = binding_domain(rec_type); + unsigned arity = get_arity(new_type); + // introduce minor arguments + buffer minor_args; + for (unsigned i = 0; i < arity; i++) { + expr arg_type = binding_domain(new_type); + name arg_name; + if (m_ids) { + arg_name = head(m_ids); + m_ids = tail(m_ids); + } else { + arg_name = binding_name(new_type); + } + expr new_h = mk_local(m_ngen.next(), get_unused_name(arg_name, new_goal_hyps), + arg_type, binder_info()); + minor_args.push_back(new_h); + new_goal_hyps.push_back(new_h); + new_type = instantiate(binding_body(new_type), new_h); + } + new_type = head_beta_reduce(new_type); + buffer new_deps; + // introduce deps + for (unsigned i = 0; i < num_deps; i++) { + if (!is_pi(new_type)) + throw_ill_formed_recursor(rec_info); + expr dep_type = binding_domain(new_type); + expr new_dep = mk_local(m_ngen.next(), get_unused_name(binding_name(new_type), new_goal_hyps), + dep_type, binder_info()); + new_deps.push_back(new_dep); + new_goal_hyps.push_back(new_dep); + new_type = instantiate(binding_body(new_type), new_dep); + } + expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(new_goal_hyps, new_type)), new_goal_hyps); + goal new_g(new_meta, new_type); + new_goals.push_back(new_g); + rec = mk_app(rec, Fun(minor_args, Fun(new_deps, new_meta))); + rec_type = m_tc.whnf(instantiate(binding_body(rec_type), new_meta)).first; + curr_pos++; + } + } + if (!consumed_major) + throw_ill_formed_recursor(rec_info); + assign(g, rec); + return to_list(new_goals); } optional execute(goal const & g, expr const & h, expr const & h_type, name const & rec) { try { recursor_info rec_info = get_recursor_info(m_env, rec); - if (!validate_rec_info(g, h, h_type, rec_info)) { - throw tactic_exception(sstream() << "invalid 'induction' tactic, indices occurring in the hypothesis '" - << h << "' must be distinct variables"); - } - unsigned nindices = rec_info.get_num_indices(); buffer h_type_args; get_app_args(h_type, h_type_args); + buffer params; + for (unsigned pos : rec_info.get_params_pos()) { + if (pos >= h_type_args.size()) + throw tactic_exception("invalid 'induction' tactic, major premise type is ill-formed"); + params.push_back(h_type_args[pos]); + } buffer indices; - indices.append(nindices, h_type_args.end() - nindices); + for (unsigned pos : rec_info.get_indices_pos()) { + if (pos >= h_type_args.size()) + throw tactic_exception("invalid 'induction' tactic, major premise type is ill-formed"); + expr const & idx = h_type_args[pos]; + if (!is_local(idx)) { + throw tactic_exception(sstream() << "invalid 'induction' tactic, argument #" + << pos+1 << " of major premise '" << h << "' type is not a variable"); + } + for (unsigned i = 0; i < h_type_args.size(); i++) { + if (i != pos && is_local(h_type_args[i]) && mlocal_name(h_type_args[i]) == mlocal_name(idx)) { + throw tactic_exception(sstream() << "invalid 'induction' tactic, argument #" + << pos+1 << " of major premise '" << h << "' type is an index, " + << "but it occurs more than once"); + } + } + indices.push_back(idx); + } + if (!rec_info.has_dep_elim() && depends_on(g.get_type(), h)) { + throw tactic_exception(sstream() << "invalid 'induction' tactic, recursor '" << rec + << "' does not support dependent elimination, but conclusion " + << "depends on major premise '" << h << "'"); + } buffer hyps, non_deps, deps; g.get_hyps(hyps); split_deps(hyps, h, indices, non_deps, deps); @@ -148,10 +222,7 @@ class induction_tac { goal new_g(new_meta, new_type); expr val = mk_app(new_meta, deps); assign(g, val); - regular(m_env, m_ios) << new_g << "\n"; - goals new_gs = apply_recursor(new_g, h, h_type, rec_info); - // TODO(Leo): finish - return optional(); + return optional(apply_recursor(new_g, deps.size(), h, h_type, params, indices, rec_info)); } catch (exception const & ex) { throw tactic_exception(sstream() << "invalid 'induction' tactic, " << ex.what()); } @@ -207,8 +278,6 @@ public: tactic induction_tactic(name const & H, optional rec, list const & ids) { name rec1 = "unknown"; if (rec) rec1 = *rec; - std::cout << "induction: " << H << " " << rec1 << " " << ids << "\n"; - auto fn = [=](environment const & env, io_state const & ios, proof_state const & ps) -> optional { goals const & gs = ps.get_goals(); if (empty(gs)) { diff --git a/tests/lean/run/ind_tac.lean b/tests/lean/run/ind_tac.lean new file mode 100644 index 000000000..804f0a337 --- /dev/null +++ b/tests/lean/run/ind_tac.lean @@ -0,0 +1,91 @@ +/- +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura + +Define propositional calculus, valuation, provability, validity, prove soundness. + +This file is based on Floris van Doorn Coq files. +-/ +import data.nat data.list +open nat bool list decidable + +definition PropVar [reducible] := nat + +inductive PropF := +| Var : PropVar → PropF +| Bot : PropF +| Conj : PropF → PropF → PropF +| Disj : PropF → PropF → PropF +| Impl : PropF → PropF → PropF + +namespace PropF + notation `#`:max P:max := Var P + notation A ∨ B := Disj A B + notation A ∧ B := Conj A B + infixr `⇒`:27 := Impl + notation `⊥` := Bot + + definition Neg A := A ⇒ ⊥ + notation ~ A := Neg A + definition Top := ~⊥ + notation `⊤` := Top + definition BiImpl A B := A ⇒ B ∧ B ⇒ A + infixr `⇔`:27 := BiImpl + + definition valuation := PropVar → bool + + definition TrueQ (v : valuation) : PropF → bool + | TrueQ (# P) := v P + | TrueQ ⊥ := ff + | TrueQ (A ∨ B) := TrueQ A || TrueQ B + | TrueQ (A ∧ B) := TrueQ A && TrueQ B + | TrueQ (A ⇒ B) := bnot (TrueQ A) || TrueQ B + + definition is_true [reducible] (b : bool) := b = tt + + -- the valuation v satisfies a list of PropF, if forall (A : PropF) in Γ, + -- (TrueQ v A) is tt (the Boolean true) + definition Satisfies v Γ := ∀ A, A ∈ Γ → is_true (TrueQ v A) + definition Models Γ A := ∀ v, Satisfies v Γ → is_true (TrueQ v A) + + infix `⊨`:80 := Models + + definition Valid p := [] ⊨ p + reserve infix `⊢`:26 + + /- Provability -/ + + inductive Nc : list PropF → PropF → Prop := + infix ⊢ := Nc + | Nax : ∀ Γ A, A ∈ Γ → Γ ⊢ A + | ImpI : ∀ Γ A B, A::Γ ⊢ B → Γ ⊢ A ⇒ B + | ImpE : ∀ Γ A B, Γ ⊢ A ⇒ B → Γ ⊢ A → Γ ⊢ B + | BotC : ∀ Γ A, (~A)::Γ ⊢ ⊥ → Γ ⊢ A + | AndI : ∀ Γ A B, Γ ⊢ A → Γ ⊢ B → Γ ⊢ A ∧ B + | AndE₁ : ∀ Γ A B, Γ ⊢ A ∧ B → Γ ⊢ A + | AndE₂ : ∀ Γ A B, Γ ⊢ A ∧ B → Γ ⊢ B + | OrI₁ : ∀ Γ A B, Γ ⊢ A → Γ ⊢ A ∨ B + | OrI₂ : ∀ Γ A B, Γ ⊢ B → Γ ⊢ A ∨ B + | OrE : ∀ Γ A B C, Γ ⊢ A ∨ B → A::Γ ⊢ C → B::Γ ⊢ C → Γ ⊢ C + + infix ⊢ := Nc + + definition Provable A := [] ⊢ A + + definition Prop_Soundness := ∀ A, Provable A → Valid A + + definition Prop_Completeness := ∀ A, Valid A → Provable A + + open Nc + + lemma weakening2 (Γ A) (H : Γ ⊢ A) (Δ) (Hs : Γ ⊆ Δ) : Δ ⊢ A := + begin + induction H, + state, + exact !Nax (Hs a), + repeat (apply sorry) + end + +end PropF diff --git a/tests/lean/run/induction_tac1.lean b/tests/lean/run/induction_tac1.lean new file mode 100644 index 000000000..fb305ad4e --- /dev/null +++ b/tests/lean/run/induction_tac1.lean @@ -0,0 +1,19 @@ +import data.vector +open vector + +set_option pp.implicit true + +attribute and.rec_on [recursor 4] + +example (a b : Prop) (h : a ∧ b) : a := +begin + induction h using and.rec_on with ha hb, + exact ha +end + +example (A : Type) (n : nat) (v w : vector A n) (h : v = w) : w = v := +begin + induction v with n a t r, + rewrite -h, + rewrite -h +end diff --git a/tests/lean/run/induction_tac2.lean b/tests/lean/run/induction_tac2.lean new file mode 100644 index 000000000..682916b63 --- /dev/null +++ b/tests/lean/run/induction_tac2.lean @@ -0,0 +1,11 @@ +import data.nat +open nat + +example (a : nat) : a + 0 = a := +begin + induction a using nat.strong_induction_on with a IH, + cases a, + reflexivity, + have aux : a + 0 = a, from IH a (lt.base a), + rewrite -aux +end diff --git a/tests/lean/user_rec_crash.lean.expected.out b/tests/lean/user_rec_crash.lean.expected.out index 83ea15216..4f945ca19 100644 --- a/tests/lean/user_rec_crash.lean.expected.out +++ b/tests/lean/user_rec_crash.lean.expected.out @@ -1,4 +1,3 @@ -induction: h and.rec_on (h₁ h₂) user_rec_crash.lean:3:2: error:invalid 'induction' tactic, invalid user defined recursor, 'and.rec_on' does not support dependent elimination, and position of the major premise was not specified (solution: set attribute '[recursor ]', where is the position of the major premise) proof state: a b : Prop,