Nuprl Lemma : combine-list-as-reduce

[A:Type]. ∀[f:A ⟶ A ⟶ A].
  (∀[L:A List]
     combine-list(x,y.f[x;y];L) outl(reduce(λx,y. case of inl(z) => inl f[x;z] inr(z) => inl x;inr ⋅ ;L)) ∈ 
     supposing 0 < ||L||) supposing 
     (Comm(A;λx,y. f[x;y]) and 
     Assoc(A;λx,y. f[x;y]))


Proof




Definitions occuring in Statement :  combine-list: combine-list(x,y.f[x; y];L) length: ||as|| reduce: reduce(f;k;as) list: List comm: Comm(T;op) assoc: Assoc(T;op) outl: outl(x) less_than: a < b it: uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s1;s2] lambda: λx.A[x] function: x:A ⟶ B[x] decide: case of inl(x) => s[x] inr(y) => t[y] inr: inr  inl: inl x natural_number: $n universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a all: x:A. B[x] or: P ∨ Q assert: b ifthenelse: if then else fi  btrue: tt less_than: a < b squash: T less_than': less_than'(a;b) false: False and: P ∧ Q cons: [a b] top: Top bfalse: ff not: ¬A implies:  Q prop: exists: x:A. B[x] nat: ge: i ≥  satisfiable_int_formula: satisfiable_int_formula(fmla) subtype_rel: A ⊆B isl: isl(x) colength: colength(L) so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] guard: {T} decidable: Dec(P) nil: [] it: so_lambda: λ2x.t[x] so_apply: x[s] sq_type: SQType(T) nat_plus: + true: True uiff: uiff(P;Q) iff: ⇐⇒ Q rev_implies:  Q append: as bs so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3] outl: outl(x) le: A ≤ B combine-list: combine-list(x,y.f[x; y];L) comm: Comm(T;op) infix_ap: y
Lemmas referenced :  last_lemma list-cases null_nil_lemma length_of_nil_lemma product_subtype_list null_cons_lemma length_of_cons_lemma false_wf nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf less_than_wf length_wf equal-wf-T-base nat_wf colength_wf_list int_subtype_base reduce_nil_lemma spread_cons_lemma intformeq_wf itermAdd_wf int_formula_prop_eq_lemma int_term_value_add_lemma decidable__le intformnot_wf int_formula_prop_not_lemma le_wf equal_wf subtract_wf itermSubtract_wf int_term_value_subtract_lemma subtype_base_sq set_subtype_base decidable__equal_int reduce_cons_lemma bool_wf bool_subtype_base reduce_wf unit_wf2 it_wf btrue_wf list_wf comm_wf assoc_wf last_wf append_wf cons_wf nil_wf length-append add_nat_plus length_wf_nat nat_plus_wf nat_plus_properties decidable__lt add-is-int-iff outl_wf assert_of_tt squash_wf true_wf combine-list-append subtype_rel_self iff_weakening_equal list_ind_cons_lemma list_ind_nil_lemma combine-list_wf non_neg_length assert_wf isl_wf list_induction reduce_hd_cons_lemma reduce_tl_cons_lemma list_accum_nil_lemma list_accum_cons_lemma list_accum_wf combine-list-cons and_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_functionElimination independent_isectElimination hypothesis unionElimination sqequalRule imageElimination productElimination voidElimination promote_hyp hypothesis_subsumption isect_memberEquality voidEquality lambdaFormation setElimination rename intWeakElimination natural_numberEquality approximateComputation independent_functionElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality independent_pairFormation axiomSqEquality applyEquality because_Cache equalityTransitivity equalitySymmetry applyLambdaEquality dependent_set_memberEquality addEquality baseClosed instantiate cumulativity unionEquality inlEquality inrEquality axiomEquality functionEquality universeEquality hyp_replacement imageMemberEquality pointwiseFunctionality baseApply closedConclusion functionExtensionality

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
    (\mforall{}[L:A  List]
          combine-list(x,y.f[x;y];L)
          =  outl(reduce(\mlambda{}x,y.  case  y  of  inl(z)  =>  inl  f[x;z]  |  inr(z)  =>  inl  x;inr  \mcdot{}  ;L)) 
          supposing  0  <  ||L||)  supposing 
          (Comm(A;\mlambda{}x,y.  f[x;y])  and 
          Assoc(A;\mlambda{}x,y.  f[x;y]))



Date html generated: 2019_06_20-PM-01_30_30
Last ObjectModification: 2018_08_21-PM-01_55_59

Theory : list_1


Home Index