michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/tactic/constructor_tactic): use 'fapply' in 'constructor' tactic

Browse source 
closes #676
This commit is contained in:
Leonardo de Moura 2015-06-16 12:03:31 -07:00
parent 2277b170f6
commit 0ae24faae3
5 changed files with 26 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/tactic/apply_tactic.cpp
View file

@ -185,6 +185,12 @@ proof_state_seq apply_tactic_core(environment const & env, io_state const & ios,
return apply_tactic_core(env, ios, s, e, tmp_cs, AddDiff, AddSubgoals);
}
proof_state_seq fapply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & e, constraint_seq const & cs) {
buffer<constraint> tmp_cs;
cs.linearize(tmp_cs);
return apply_tactic_core(env, ios, s, e, tmp_cs, AddDiff, AddAllSubgoals);
}
tactic apply_tactic_core(expr const & e, constraint_seq const & cs) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
return apply_tactic_core(env, ios, s, e, cs);

1
src/library/tactic/apply_tactic.h
View file

@ -9,6 +9,7 @@ Author: Leonardo de Moura
#include "library/tactic/elaborate.h"
namespace lean {
proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & e, constraint_seq const & cs);
proof_state_seq fapply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & e, constraint_seq const & cs);
tactic apply_tactic_core(expr const & e, constraint_seq const & cs = constraint_seq());
tactic apply_tactic(elaborate_fn const & fn, expr const & e);
tactic fapply_tactic(elaborate_fn const & fn, expr const & e);

2
src/library/tactic/constructor_tactic.cpp
View file

@ -83,7 +83,7 @@ tactic constructor_tactic(elaborate_fn const & elab, optional<unsigned> _i, opti
return proof_state_seq();
}
}
return apply_tactic_core(env, ios, new_s, C, cs);
return fapply_tactic_core(env, ios, new_s, C, cs);
};
if (_i) {

12
tests/lean/run/676.lean Normal file
View file

@ -0,0 +1,12 @@
import data.nat
open nat
inductive foo : Prop :=
mk : ∀ {a : nat}, a > 0 → foo
example (b : nat) (h : b > 1) : foo :=
begin
constructor,
exact b,
exact lt_of_succ_lt h
end

12
tests/lean/run/soundness.lean
View file

@ -90,26 +90,26 @@ namespace PropF
lemma weakening2 : ∀ {Γ A Δ}, Γ ⊢ A → Γ ⊆ Δ → Δ ⊢ A
| Γ ⌞A⌟ Δ (Nax Γ A Hin) Hs := by constructor; exact Hs Hin
| Γ ⌞A ⇒ B⌟ Δ (ImpI Γ A B H) Hs := by constructor; exact weakening2 H (cons_sub_cons A Hs)
| Γ ⌞B⌟ Δ (ImpE Γ A B H₁ H₂) Hs := by constructor; exact weakening2 H₁ Hs; exact weakening2 H₂ Hs
| Γ ⌞B⌟ Δ (ImpE Γ A B H₁ H₂) Hs := by constructor; eassumption; exact weakening2 H₁ Hs; exact weakening2 H₂ Hs
| Γ ⌞A⌟ Δ (BotC Γ A H) Hs := by constructor; exact weakening2 H (cons_sub_cons (~A) Hs)
| Γ ⌞A ∧ B⌟ Δ (AndI Γ A B H₁ H₂) Hs := by constructor; exact weakening2 H₁ Hs; exact weakening2 H₂ Hs
| Γ ⌞A⌟ Δ (AndE₁ Γ A B H) Hs := by constructor; exact weakening2 H Hs
| Γ ⌞B⌟ Δ (AndE₂ Γ A B H) Hs := by constructor; exact weakening2 H Hs
| Γ ⌞A⌟ Δ (AndE₁ Γ A B H) Hs := by constructor; eassumption; exact weakening2 H Hs
| Γ ⌞B⌟ Δ (AndE₂ Γ A B H) Hs := by constructor; eassumption; exact weakening2 H Hs
| Γ ⌞A ∨ B⌟ Δ (OrI₁ Γ A B H) Hs := by constructor; exact weakening2 H Hs
| Γ ⌞A ∨ B⌟ Δ (OrI₂ Γ A B H) Hs := by constructor; exact weakening2 H Hs
| Γ ⌞C⌟ Δ (OrE Γ A B C H₁ H₂ H₃) Hs :=
by constructor; exact weakening2 H₁ Hs; exact weakening2 H₂ (cons_sub_cons A Hs); exact weakening2 H₃ (cons_sub_cons B Hs)
by constructor; eassumption; eassumption; exact weakening2 H₁ Hs; exact weakening2 H₂ (cons_sub_cons A Hs); exact weakening2 H₃ (cons_sub_cons B Hs)
lemma weakening : ∀ Γ Δ A, Γ ⊢ A → Γ++Δ ⊢ A :=
λ Γ Δ A H, weakening2 H (sub_append_left Γ Δ)
lemma deduction : ∀ Γ A B, Γ ⊢ A ⇒ B → A::Γ ⊢ B :=
λ Γ A B H, by constructor; exact weakening2 H (sub_cons A Γ); constructor; exact mem_cons A Γ
λ Γ A B H, by constructor; exact A; exact weakening2 H (sub_cons A Γ); constructor; exact mem_cons A Γ
lemma prov_impl : ∀ A B, Provable (A ⇒ B) → ∀ Γ, Γ ⊢ A → Γ ⊢ B :=
λ A B Hp Γ Ha,
assert wHp : Γ ⊢ (A ⇒ B), from !weakening Hp,
by constructor; eassumption; eassumption
by constructor; eassumption; eassumption; eassumption
lemma Satisfies_cons : ∀ {A Γ v}, Satisfies v Γ → is_true (TrueQ v A) → Satisfies v (A::Γ) :=
λ A Γ v s t B BinAG,