Commit e9679e64 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

cleanup in Nam.valid_deriv_step

parent ec7f8f1e
...@@ -161,6 +161,8 @@ Proof. ...@@ -161,6 +161,8 @@ Proof.
rewrite nam2mix_fvars. simpl. namedec. rewrite nam2mix_fvars. simpl. namedec.
- rewrite nam2mix_subst_bsubst0; auto. - rewrite nam2mix_subst_bsubst0; auto.
- rewrite nam2mix_subst_bsubst0; auto. - rewrite nam2mix_subst_bsubst0; auto.
rewrite <- !andb_lazy_alt. f_equal.
apply eq_true_iff_eq. now rewrite !eqb_eq.
- cbn. - cbn.
apply eq_true_iff_eq. apply eq_true_iff_eq.
rewrite !andb_true_iff. rewrite !andb_true_iff.
......
...@@ -432,9 +432,10 @@ Inductive derivation := ...@@ -432,9 +432,10 @@ Inductive derivation :=
Definition claim '(Rule _ s _) := s. Definition claim '(Rule _ s _) := s.
Definition valid_deriv_step logic '(Rule r s ld) := Definition valid_deriv_step logic '(Rule rule stmt subderivs) :=
match r, s, List.map claim ld with let premises := List.map claim subderivs in
| Ax, (Γ ⊢ A), [] => List.existsb (Form.αeq A) Γ match rule, stmt, premises with
| Ax, (Γ ⊢ A), [] => List.existsb (fun F => A =? F) Γ
| Tr_i, (_ ⊢ True), [] => true | Tr_i, (_ ⊢ True), [] => true
| Fa_e, (Γ ⊢ _), [s] => s =? (Γ ⊢ False) | Fa_e, (Γ ⊢ _), [s] => s =? (Γ ⊢ False)
| Not_i, (Γ ⊢ Not A), [s] => s =? (A::Γ ⊢ False) | Not_i, (Γ ⊢ Not A), [s] => s =? (A::Γ ⊢ False)
...@@ -453,10 +454,8 @@ Definition valid_deriv_step logic '(Rule r s ld) := ...@@ -453,10 +454,8 @@ Definition valid_deriv_step logic '(Rule r s ld) :=
(s =? (Γ ⊢ B)) &&& (s2 =? (Γ ⊢ A)) (s =? (Γ ⊢ B)) &&& (s2 =? (Γ ⊢ A))
| All_i x, s, [Γ ⊢ A] => | All_i x, s, [Γ ⊢ A] =>
(s =? (Γ ⊢ ∀x,A)) &&& negb (Names.mem x (Ctx.freevars Γ)) (s =? (Γ ⊢ ∀x,A)) &&& negb (Names.mem x (Ctx.freevars Γ))
| All_e t, (Γ ⊢ B), [Γ'⊢ ∀x,A] => | All_e t, s, [Γ ⊢ ∀x,A] => s =? (Γ ⊢ Form.subst x t A)
(Γ =? Γ') &&& (B =? Form.subst x t A) | Ex_i t, (Γ ⊢ ∃x,A), [s] => s =? (Γ ⊢ Form.subst x t A)
| Ex_i t, (Γ ⊢ ∃x,A), [Γ'⊢B] =>
(Γ =? Γ') &&& (B =? Form.subst x t A)
| Ex_e x, s, [s1; A::Γ ⊢ B] => | Ex_e x, s, [s1; A::Γ ⊢ B] =>
(s =? (Γ ⊢ B)) &&& (s1 =? (Γ ⊢ ∃x, A)) &&& (s =? (Γ ⊢ B)) &&& (s1 =? (Γ ⊢ ∃x, A)) &&&
negb (Names.mem x (Seq.freevars s)) negb (Names.mem x (Seq.freevars s))
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment