PP0027

prime_field_polynomial_horner_normalization_residue

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Ordinary induction proves the residue invariant against arbitrary natural coefficients and their actual coefficientwise reduction; the invariant is not part of the execution definition.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Exact expanded first-order arithmetic statement

forall p b c d e t l n r. (~((p) = 1) /\ forall pfa_factor_left_invariant_prime pfa_factor_right_invariant_prime. (p) = pfa_factor_left_invariant_prime * pfa_factor_right_invariant_prime -> pfa_factor_left_invariant_prime = 1 \/ pfa_factor_right_invariant_prime = 1) -> (forall pfp_index_invariant_coefficients_reduced. (exists pfa_gap_invariant_coefficients_reducedindex. pfa_gap_invariant_coefficients_reducedindex + S (pfp_index_invariant_coefficients_reduced) = (l)) -> exists pfp_source_invariant_coefficients_reduced pfp_residue_invariant_coefficients_reduced. ((((exists ff_h_pfp_invariant_coefficients_reducedsource. ff_h_pfp_invariant_coefficients_reducedsource + S (pfp_source_invariant_coefficients_reduced) = S ((S (pfp_index_invariant_coefficients_reduced)) * c)) /\ exists ff_q_pfp_invariant_coefficients_reducedsource. b = ff_q_pfp_invariant_coefficients_reducedsource * S ((S (pfp_index_invariant_coefficients_reduced)) * c) + (pfp_source_invariant_coefficients_reduced))) /\ (((((exists ff_h_pfp_invariant_coefficients_reducedtarget. ff_h_pfp_invariant_coefficients_reducedtarget + S (pfp_residue_invariant_coefficients_reduced) = S ((S (pfp_index_invariant_coefficients_reduced)) * e)) /\ exists ff_q_pfp_invariant_coefficients_reducedtarget. d = ff_q_pfp_invariant_coefficients_reducedtarget * S ((S (pfp_index_invariant_coefficients_reduced)) * e) + (pfp_residue_invariant_coefficients_reduced))) /\ ((((exists pfa_gap_invariant_coefficients_reducedresiduebound. pfa_gap_invariant_coefficients_reducedresiduebound + S (pfp_residue_invariant_coefficients_reduced) = (p)) /\ ((exists pfa_offset_left_invariant_coefficients_reducedresiduecongruence pfa_offset_right_invariant_coefficients_reducedresiduecongruence. (pfp_source_invariant_coefficients_reduced) + (p) * pfa_offset_left_invariant_coefficients_reducedresiduecongruence = (pfp_residue_invariant_coefficients_reduced) + (p) * pfa_offset_right_invariant_coefficients_reducedresiduecongruence))))))))) -> (exists ff_u_ph_pfh_invariant_natural ff_v_ph_pfh_invariant_natural. ((((exists fs_h_ph_pfh_invariant_natural_body_start. fs_h_ph_pfh_invariant_natural_body_start + S (0) = S ((S (0)) * ff_v_ph_pfh_invariant_natural)) /\ exists fs_q_ph_pfh_invariant_natural_body_start. ff_u_ph_pfh_invariant_natural = fs_q_ph_pfh_invariant_natural_body_start * S ((S (0)) * ff_v_ph_pfh_invariant_natural) + (0))) /\ ((((exists fs_h_ph_pfh_invariant_natural_body_terminal. fs_h_ph_pfh_invariant_natural_body_terminal + S (n) = S ((S (l)) * ff_v_ph_pfh_invariant_natural)) /\ exists fs_q_ph_pfh_invariant_natural_body_terminal. ff_u_ph_pfh_invariant_natural = fs_q_ph_pfh_invariant_natural_body_terminal * S ((S (l)) * ff_v_ph_pfh_invariant_natural) + (n))) /\ forall ff_i_ph_pfh_invariant_natural_body_steps. (exists ph_bound_pfh_invariant_natural_body_steps. ph_bound_pfh_invariant_natural_body_steps + S ff_i_ph_pfh_invariant_natural_body_steps = l) -> exists ff_coefficient_ph_pfh_invariant_natural_body_steps ff_previous_ph_pfh_invariant_natural_body_steps ff_current_ph_pfh_invariant_natural_body_steps. ((((exists fs_h_ph_pfh_invariant_natural_body_steps_coefficient. fs_h_ph_pfh_invariant_natural_body_steps_coefficient + S (ff_coefficient_ph_pfh_invariant_natural_body_steps) = S ((S (ff_i_ph_pfh_invariant_natural_body_steps)) * c)) /\ exists fs_q_ph_pfh_invariant_natural_body_steps_coefficient. b = fs_q_ph_pfh_invariant_natural_body_steps_coefficient * S ((S (ff_i_ph_pfh_invariant_natural_body_steps)) * c) + (ff_coefficient_ph_pfh_invariant_natural_body_steps))) /\ ((((exists fs_h_ph_pfh_invariant_natural_body_steps_before. fs_h_ph_pfh_invariant_natural_body_steps_before + S (ff_previous_ph_pfh_invariant_natural_body_steps) = S ((S (ff_i_ph_pfh_invariant_natural_body_steps)) * ff_v_ph_pfh_invariant_natural)) /\ exists fs_q_ph_pfh_invariant_natural_body_steps_before. ff_u_ph_pfh_invariant_natural = fs_q_ph_pfh_invariant_natural_body_steps_before * S ((S (ff_i_ph_pfh_invariant_natural_body_steps)) * ff_v_ph_pfh_invariant_natural) + (ff_previous_ph_pfh_invariant_natural_body_steps))) /\ ((((exists fs_h_ph_pfh_invariant_natural_body_steps_after. fs_h_ph_pfh_invariant_natural_body_steps_after + S (ff_current_ph_pfh_invariant_natural_body_steps) = S ((S (S ff_i_ph_pfh_invariant_natural_body_steps)) * ff_v_ph_pfh_invariant_natural)) /\ exists fs_q_ph_pfh_invariant_natural_body_steps_after. ff_u_ph_pfh_invariant_natural = fs_q_ph_pfh_invariant_natural_body_steps_after * S ((S (S ff_i_ph_pfh_invariant_natural_body_steps)) * ff_v_ph_pfh_invariant_natural) + (ff_current_ph_pfh_invariant_natural_body_steps))) /\ ff_current_ph_pfh_invariant_natural_body_steps = ff_previous_ph_pfh_invariant_natural_body_steps * t + ff_coefficient_ph_pfh_invariant_natural_body_steps)))))) -> (exists pfh_trace_code_invariant_execution pfh_trace_scale_invariant_execution. (((exists pfa_gap_invariant_executiontracebase. pfa_gap_invariant_executiontracebase + S (t) = (p)) /\ (((((exists ff_h_pfp_invariant_executiontraceinitial. ff_h_pfp_invariant_executiontraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_invariant_execution)) /\ exists ff_q_pfp_invariant_executiontraceinitial. pfh_trace_code_invariant_execution = ff_q_pfp_invariant_executiontraceinitial * S ((S (0)) * pfh_trace_scale_invariant_execution) + (0))) /\ (((((exists ff_h_pfp_invariant_executiontraceterminal. ff_h_pfp_invariant_executiontraceterminal + S (r) = S ((S (l)) * pfh_trace_scale_invariant_execution)) /\ exists ff_q_pfp_invariant_executiontraceterminal. pfh_trace_code_invariant_execution = ff_q_pfp_invariant_executiontraceterminal * S ((S (l)) * pfh_trace_scale_invariant_execution) + (r))) /\ ((forall pfh_index_invariant_executiontracesteps. (exists pfa_gap_invariant_executiontracestepsindex. pfa_gap_invariant_executiontracestepsindex + S (pfh_index_invariant_executiontracesteps) = (l)) -> (exists pfh_coefficient_invariant_executiontracestepsstep pfh_before_invariant_executiontracestepsstep pfh_after_invariant_executiontracestepsstep pfh_product_invariant_executiontracestepsstep. ((((exists ff_h_pfp_invariant_executiontracestepsstepcoefficient. ff_h_pfp_invariant_executiontracestepsstepcoefficient + S (pfh_coefficient_invariant_executiontracestepsstep) = S ((S (pfh_index_invariant_executiontracesteps)) * e)) /\ exists ff_q_pfp_invariant_executiontracestepsstepcoefficient. d = ff_q_pfp_invariant_executiontracestepsstepcoefficient * S ((S (pfh_index_invariant_executiontracesteps)) * e) + (pfh_coefficient_invariant_executiontracestepsstep))) /\ (((((exists ff_h_pfp_invariant_executiontracestepsstepbefore. ff_h_pfp_invariant_executiontracestepsstepbefore + S (pfh_before_invariant_executiontracestepsstep) = S ((S (pfh_index_invariant_executiontracesteps)) * pfh_trace_scale_invariant_execution)) /\ exists ff_q_pfp_invariant_executiontracestepsstepbefore. pfh_trace_code_invariant_execution = ff_q_pfp_invariant_executiontracestepsstepbefore * S ((S (pfh_index_invariant_executiontracesteps)) * pfh_trace_scale_invariant_execution) + (pfh_before_invariant_executiontracestepsstep))) /\ (((((exists ff_h_pfp_invariant_executiontracestepsstepafter. ff_h_pfp_invariant_executiontracestepsstepafter + S (pfh_after_invariant_executiontracestepsstep) = S ((S (S (pfh_index_invariant_executiontracesteps))) * pfh_trace_scale_invariant_execution)) /\ exists ff_q_pfp_invariant_executiontracestepsstepafter. pfh_trace_code_invariant_execution = ff_q_pfp_invariant_executiontracestepsstepafter * S ((S (S (pfh_index_invariant_executiontracesteps))) * pfh_trace_scale_invariant_execution) + (pfh_after_invariant_executiontracestepsstep))) /\ (((((exists pfa_gap_invariant_executiontracestepsstepmultiplyleft. pfa_gap_invariant_executiontracestepsstepmultiplyleft + S (pfh_before_invariant_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_invariant_executiontracestepsstepmultiplyright. pfa_gap_invariant_executiontracestepsstepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_invariant_executiontracestepsstepmultiplyresultbound. pfa_gap_invariant_executiontracestepsstepmultiplyresultbound + S (pfh_product_invariant_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_invariant_executiontracestepsstepmultiplyresultcongruence pfa_offset_right_invariant_executiontracestepsstepmultiplyresultcongruence. ((pfh_before_invariant_executiontracestepsstep) * (t)) + (p) * pfa_offset_left_invariant_executiontracestepsstepmultiplyresultcongruence = (pfh_product_invariant_executiontracestepsstep) + (p) * pfa_offset_right_invariant_executiontracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_invariant_executiontracestepsstepaddleft. pfa_gap_invariant_executiontracestepsstepaddleft + S (pfh_product_invariant_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_invariant_executiontracestepsstepaddright. pfa_gap_invariant_executiontracestepsstepaddright + S (pfh_coefficient_invariant_executiontracestepsstep) = (p)) /\ ((((exists pfa_gap_invariant_executiontracestepsstepaddresultbound. pfa_gap_invariant_executiontracestepsstepaddresultbound + S (pfh_after_invariant_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_invariant_executiontracestepsstepaddresultcongruence pfa_offset_right_invariant_executiontracestepsstepaddresultcongruence. ((pfh_product_invariant_executiontracestepsstep) + (pfh_coefficient_invariant_executiontracestepsstep)) + (p) * pfa_offset_left_invariant_executiontracestepsstepaddresultcongruence = (pfh_after_invariant_executiontracestepsstep) + (p) * pfa_offset_right_invariant_executiontracestepsstepaddresultcongruence))))))))))))))))))))))))))) -> (((exists pfa_gap_invariant_resultbound. pfa_gap_invariant_resultbound + S (r) = (p)) /\ ((exists pfa_offset_left_invariant_resultcongruence pfa_offset_right_invariant_resultcongruence. (n) + (p) * pfa_offset_left_invariant_resultcongruence = (r) + (p) * pfa_offset_right_invariant_resultcongruence))))

Constructive proof overview

Generated structural guide

Ordinary induction proves the residue invariant against arbitrary natural coefficients and their actual coefficientwise reduction; the invariant is not part of the execution definition.

The unchanged tactic script uses 13 declared prerequisites and contains 142 exact native proof lines.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

beta_horner_eval_empty Alpha theorem; checked-use authorized PP0024 prime_field_polynomial_horner_empty prime_field_residue_reflexive Alpha theorem; checked-use authorized prime_field_zero_below_prime Alpha theorem; checked-use authorized beta_horner_eval_successor_decompose Alpha theorem; checked-use authorized PP0025 prime_field_polynomial_horner_successor_decompose PP0003 prime_field_polynomial_normalization_entry zero_add Stable theorem; checked-use authorized le_succ Stable theorem; checked-use authorized PP0023 prime_field_polynomial_horner_input_bounds prime_field_residue_multiply Alpha theorem; checked-use authorized prime_field_residue_input_equal Alpha theorem; checked-use authorized prime_field_residue_add Alpha theorem; checked-use authorized

Direct dependents

PP0028 prime_field_polynomial_horner_residue PP002F prime_field_polynomial_normalized_horner_iff PP0031 prime_field_polynomial_reduce_and_evaluate_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

142 script commands · 22 reading checkpoints · 8 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (4)
prime field polynomial horner emptyprime field polynomial horner successor decomposeprime field polynomial normalization entryprime field polynomial horner input bounds

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–7

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro d
  5. L5
    intro e
  6. L6
    intro t
  7. L7
    intro l
02Induction on lL8–14

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L8
    induction l
  2. L9
    intro n
  3. L10
    intro r
  4. L11
    intro hp
  5. L12
    intro hred
  6. L13
    intro hn
  7. L14
    intro hr
03Establish hnzeroL15–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta horner eval empty.

  1. L15
    have hnzero : n=0
  2. L16
    specialize beta_horner_eval_empty (b)
  3. L17
    specialize beta_horner_eval_empty (c)
  4. L18
    specialize beta_horner_eval_empty (t)
  5. L19
    specialize beta_horner_eval_empty (n)
  6. L20
    apply beta_horner_eval_empty
  7. L21
    exact hn
04Establish hrzeroL22–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial horner empty.

  1. L22
    have hrzero : r=0
  2. L23
    specialize prime_field_polynomial_horner_empty (p)
  3. L24
    specialize prime_field_polynomial_horner_empty (d)
  4. L25
    specialize prime_field_polynomial_horner_empty (e)
  5. L26
    specialize prime_field_polynomial_horner_empty (t)
  6. L27
    specialize prime_field_polynomial_horner_empty (r)
  7. L28
    apply prime_field_polynomial_horner_empty
  8. L29
    exact hr
  9. L30
    rewrite hnzero
  10. L31
    rewrite hrzero
05Calculate and transport equalitiesL32–32

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L32
    rewrite hrzero
06Use earlier factsL33–38

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L33
    specialize prime_field_residue_reflexive (p)
  2. L34
    specialize prime_field_residue_reflexive (0)
  3. L35
    apply prime_field_residue_reflexive
  4. L36
    specialize prime_field_zero_below_prime (p)
  5. L37
    apply prime_field_zero_below_prime
  6. L38
    exact hp
07Fix variables and assumptionsL39–44

Work with arbitrary variables or the premises of the current implication.

  1. L39
    intro n
  2. L40
    intro r
  3. L41
    intro hp
  4. L42
    intro hred
  5. L43
    intro hn
  6. L44
    intro hr
08Establish hnsL45–52

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta horner eval successor decompose.

  1. L45
    have hns : ∃ a. ∃ h. BetaAt(b,c,l,a) ∧ (Horner(b,c,t,l,h) ∧ n = h · t + a)Definitions: HornerBetaAt
  2. L46
    specialize beta_horner_eval_successor_decompose (b)
  3. L47
    specialize beta_horner_eval_successor_decompose (c)
  4. L48
    specialize beta_horner_eval_successor_decompose (t)
  5. L49
    specialize beta_horner_eval_successor_decompose (l)
  6. L50
    specialize beta_horner_eval_successor_decompose (n)
  7. L51
    apply beta_horner_eval_successor_decompose
  8. L52
    exact hn
09Separate the logical casesL53–56

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L53
    cases hns
  2. L54
    cases hns_witness
  3. L55
    cases hns_witness_witness
  4. L56
    cases hns_witness_witness_right
10Establish hrsL57–65

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial horner successor decompose.

  1. L57
    have hrs : ∃ a. ∃ h. ∃ k. BetaAt(d,e,l,a) ∧ (FpHorner(p,d,e,t,l,h) ∧ (FpMul(p,h,t,k) ∧ FpAdd(p,k,a,r)))Definitions: FpAddFpMulFpHornerBetaAt
  2. L58
    specialize prime_field_polynomial_horner_successor_decompose (p)
  3. L59
    specialize prime_field_polynomial_horner_successor_decompose (d)
  4. L60
    specialize prime_field_polynomial_horner_successor_decompose (e)
  5. L61
    specialize prime_field_polynomial_horner_successor_decompose (t)
  6. L62
    specialize prime_field_polynomial_horner_successor_decompose (l)
  7. L63
    specialize prime_field_polynomial_horner_successor_decompose (r)
  8. L64
    apply prime_field_polynomial_horner_successor_decompose
  9. L65
    exact hr
11Separate the logical casesL66–71

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L66
    cases hrs
  2. L67
    cases hrs_witness
  3. L68
    cases hrs_witness_witness
  4. L69
    cases hrs_witness_witness_witness
  5. L70
    cases hrs_witness_witness_witness_right
  6. L71
    cases hrs_witness_witness_witness_right_right
12Establish hcoefficientL72–81

Establish this local claim before using it. It is not an additional assumption.

  1. L72
    have hcoefficient : ((exists pfa_gap_invariant_coefficient_residuebound. pfa_gap_invariant_coefficient_residuebound + S (x2) = (p)) /\ ((exists pfa_offset_left_invariant_coefficient_residuecongruence pfa_offset_right_invariant_coefficient_residuecongruence. (x) + (p) * pfa_offset_left_invariant_coefficient_residuecongruence = (x2) + (p) * pfa_offset_right_invariant_coefficient_residuecongruence)))
  2. L73
    specialize prime_field_polynomial_normalization_entry (p)
  3. L74
    specialize prime_field_polynomial_normalization_entry (b)
  4. L75
    specialize prime_field_polynomial_normalization_entry (c)
  5. L76
    specialize prime_field_polynomial_normalization_entry (d)
  6. L77
    specialize prime_field_polynomial_normalization_entry (e)
  7. L78
    specialize prime_field_polynomial_normalization_entry (S l)
  8. L79
    specialize prime_field_polynomial_normalization_entry (l)
  9. L80
    specialize prime_field_polynomial_normalization_entry (x)
  10. L81
    specialize prime_field_polynomial_normalization_entry (x2)
13Use earlier factsL82–83

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L82
    apply prime_field_polynomial_normalization_entry
  2. L83
    exact hred
14Construct an explicit witnessL84–84

Supply the displayed value, then prove that it has the required property.

  1. L84
    exists 0
15Use earlier factsL85–87

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L85
    apply zero_add
  2. L86
    exact hns_witness_witness_left
  3. L87
    exact hrs_witness_witness_witness_left
16Establish hpreviousL88–97

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.

  1. L88
    have hprevious : ((exists pfa_gap_invariant_previous_residuebound. pfa_gap_invariant_previous_residuebound + S (x3) = (p)) /\ ((exists pfa_offset_left_invariant_previous_residuecongruence pfa_offset_right_invariant_previous_residuecongruence. (x1) + (p) * pfa_offset_left_invariant_previous_residuecongruence = (x3) + (p) * pfa_offset_right_invariant_previous_residuecongruence)))
  2. L89
    specialize IH (x1)
  3. L90
    specialize IH (x3)
  4. L91
    apply IH
  5. L92
    exact hp
  6. L93
    intro i
  7. L94
    intro hi
  8. L95
    specialize hred (i)
  9. L96
    apply hred
  10. L97
    specialize le_succ (S i)
17Use earlier factsL98–102

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L98
    specialize le_succ (l)
  2. L99
    apply le_succ
  3. L100
    exact hi
  4. L101
    exact hns_witness_witness_right_left
  5. L102
    exact hrs_witness_witness_witness_right_left
18Establish hboundsL103–111

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial horner input bounds.

  1. L103
    have hbounds : Lt(t,p) ∧ BetaPrefixInto(d,e,l,p)Definitions: BetaPrefixIntoLt
  2. L104
    specialize prime_field_polynomial_horner_input_bounds (p)
  3. L105
    specialize prime_field_polynomial_horner_input_bounds (d)
  4. L106
    specialize prime_field_polynomial_horner_input_bounds (e)
  5. L107
    specialize prime_field_polynomial_horner_input_bounds (t)
  6. L108
    specialize prime_field_polynomial_horner_input_bounds (l)
  7. L109
    specialize prime_field_polynomial_horner_input_bounds (x3)
  8. L110
    apply prime_field_polynomial_horner_input_bounds
  9. L111
    exact hrs_witness_witness_witness_right_left
19Separate the logical casesL112–112

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L112
    cases hbounds
20Establish hproductL113–122

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field residue multiply.

  1. L113
    have hproduct : ((exists pfa_gap_invariant_product_residuebound. pfa_gap_invariant_product_residuebound + S (x4) = (p)) /\ ((exists pfa_offset_left_invariant_product_residuecongruence pfa_offset_right_invariant_product_residuecongruence. (x1*t) + (p) * pfa_offset_left_invariant_product_residuecongruence = (x4) + (p) * pfa_offset_right_invariant_product_residuecongruence)))
  2. L114
    specialize prime_field_residue_multiply (p)
  3. L115
    specialize prime_field_residue_multiply (x1)
  4. L116
    specialize prime_field_residue_multiply (t)
  5. L117
    specialize prime_field_residue_multiply (x3)
  6. L118
    specialize prime_field_residue_multiply (t)
  7. L119
    specialize prime_field_residue_multiply (x4)
  8. L120
    apply prime_field_residue_multiply
  9. L121
    exact hprevious
  10. L122
    specialize prime_field_residue_reflexive (p)
21Use earlier factsL123–132

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L123
    specialize prime_field_residue_reflexive (t)
  2. L124
    apply prime_field_residue_reflexive
  3. L125
    exact hbounds_left
  4. L126
    exact hrs_witness_witness_witness_right_right_left
  5. L127
    specialize prime_field_residue_input_equal (p)
  6. L128
    specialize prime_field_residue_input_equal (n)
  7. L129
    specialize prime_field_residue_input_equal (x1*t+x)
  8. L130
    specialize prime_field_residue_input_equal (r)
  9. L131
    apply prime_field_residue_input_equal
  10. L132
    exact hns_witness_witness_right_right
22Use earlier factsL133–142

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L133
    specialize prime_field_residue_add (p)
  2. L134
    specialize prime_field_residue_add (x1*t)
  3. L135
    specialize prime_field_residue_add (x)
  4. L136
    specialize prime_field_residue_add (x4)
  5. L137
    specialize prime_field_residue_add (x2)
  6. L138
    specialize prime_field_residue_add (r)
  7. L139
    apply prime_field_residue_add
  8. L140
    exact hproduct
  9. L141
    exact hcoefficient
  10. L142
    exact hrs_witness_witness_witness_right_right_right

Library-wide reading audit

Original exact command ledger · 142 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro e
  6. 0006intro t
  7. 0007intro l
  8. 0008induction l
  9. 0009intro n
  10. 0010intro r
  11. 0011intro hp
  12. 0012intro hred
  13. 0013intro hn
  14. 0014intro hr
  15. 0015have hnzero : n=0
  16. 0016specialize beta_horner_eval_empty (b)
  17. 0017specialize beta_horner_eval_empty (c)
  18. 0018specialize beta_horner_eval_empty (t)
  19. 0019specialize beta_horner_eval_empty (n)
  20. 0020apply beta_horner_eval_empty
  21. 0021exact hn
  22. 0022have hrzero : r=0
  23. 0023specialize prime_field_polynomial_horner_empty (p)
  24. 0024specialize prime_field_polynomial_horner_empty (d)
  25. 0025specialize prime_field_polynomial_horner_empty (e)
  26. 0026specialize prime_field_polynomial_horner_empty (t)
  27. 0027specialize prime_field_polynomial_horner_empty (r)
  28. 0028apply prime_field_polynomial_horner_empty
  29. 0029exact hr
  30. 0030rewrite hnzero
  31. 0031rewrite hrzero
  32. 0032rewrite hrzero
  33. 0033specialize prime_field_residue_reflexive (p)
  34. 0034specialize prime_field_residue_reflexive (0)
  35. 0035apply prime_field_residue_reflexive
  36. 0036specialize prime_field_zero_below_prime (p)
  37. 0037apply prime_field_zero_below_prime
  38. 0038exact hp
  39. 0039intro n
  40. 0040intro r
  41. 0041intro hp
  42. 0042intro hred
  43. 0043intro hn
  44. 0044intro hr
  45. 0045have hns : exists a h. ((((exists ff_h_pfp_invariant_natural_coefficient. ff_h_pfp_invariant_natural_coefficient + S (a) = S ((S (l)) * c)) /\ exists ff_q_pfp_invariant_natural_coefficient. b = ff_q_pfp_invariant_natural_coefficient * S ((S (l)) * c) + (a))) /\ (((exists ff_u_ph_pfh_invariant_natural_prefix ff_v_ph_pfh_invariant_natural_prefix. ((((exists fs_h_ph_pfh_invariant_natural_prefix_body_start. fs_h_ph_pfh_invariant_natural_prefix_body_start + S (0) = S ((S (0)) * ff_v_ph_pfh_invariant_natural_prefix)) /\ exists fs_q_ph_pfh_invariant_natural_prefix_body_start. ff_u_ph_pfh_invariant_natural_prefix = fs_q_ph_pfh_invariant_natural_prefix_body_start * S ((S (0)) * ff_v_ph_pfh_invariant_natural_prefix) + (0))) /\ ((((exists fs_h_ph_pfh_invariant_natural_prefix_body_terminal. fs_h_ph_pfh_invariant_natural_prefix_body_terminal + S (h) = S ((S (l)) * ff_v_ph_pfh_invariant_natural_prefix)) /\ exists fs_q_ph_pfh_invariant_natural_prefix_body_terminal. ff_u_ph_pfh_invariant_natural_prefix = fs_q_ph_pfh_invariant_natural_prefix_body_terminal * S ((S (l)) * ff_v_ph_pfh_invariant_natural_prefix) + (h))) /\ forall ff_i_ph_pfh_invariant_natural_prefix_body_steps. (exists ph_bound_pfh_invariant_natural_prefix_body_steps. ph_bound_pfh_invariant_natural_prefix_body_steps + S ff_i_ph_pfh_invariant_natural_prefix_body_steps = l) -> exists ff_coefficient_ph_pfh_invariant_natural_prefix_body_steps ff_previous_ph_pfh_invariant_natural_prefix_body_steps ff_current_ph_pfh_invariant_natural_prefix_body_steps. ((((exists fs_h_ph_pfh_invariant_natural_prefix_body_steps_coefficient. fs_h_ph_pfh_invariant_natural_prefix_body_steps_coefficient + S (ff_coefficient_ph_pfh_invariant_natural_prefix_body_steps) = S ((S (ff_i_ph_pfh_invariant_natural_prefix_body_steps)) * c)) /\ exists fs_q_ph_pfh_invariant_natural_prefix_body_steps_coefficient. b = fs_q_ph_pfh_invariant_natural_prefix_body_steps_coefficient * S ((S (ff_i_ph_pfh_invariant_natural_prefix_body_steps)) * c) + (ff_coefficient_ph_pfh_invariant_natural_prefix_body_steps))) /\ ((((exists fs_h_ph_pfh_invariant_natural_prefix_body_steps_before. fs_h_ph_pfh_invariant_natural_prefix_body_steps_before + S (ff_previous_ph_pfh_invariant_natural_prefix_body_steps) = S ((S (ff_i_ph_pfh_invariant_natural_prefix_body_steps)) * ff_v_ph_pfh_invariant_natural_prefix)) /\ exists fs_q_ph_pfh_invariant_natural_prefix_body_steps_before. ff_u_ph_pfh_invariant_natural_prefix = fs_q_ph_pfh_invariant_natural_prefix_body_steps_before * S ((S (ff_i_ph_pfh_invariant_natural_prefix_body_steps)) * ff_v_ph_pfh_invariant_natural_prefix) + (ff_previous_ph_pfh_invariant_natural_prefix_body_steps))) /\ ((((exists fs_h_ph_pfh_invariant_natural_prefix_body_steps_after. fs_h_ph_pfh_invariant_natural_prefix_body_steps_after + S (ff_current_ph_pfh_invariant_natural_prefix_body_steps) = S ((S (S ff_i_ph_pfh_invariant_natural_prefix_body_steps)) * ff_v_ph_pfh_invariant_natural_prefix)) /\ exists fs_q_ph_pfh_invariant_natural_prefix_body_steps_after. ff_u_ph_pfh_invariant_natural_prefix = fs_q_ph_pfh_invariant_natural_prefix_body_steps_after * S ((S (S ff_i_ph_pfh_invariant_natural_prefix_body_steps)) * ff_v_ph_pfh_invariant_natural_prefix) + (ff_current_ph_pfh_invariant_natural_prefix_body_steps))) /\ ff_current_ph_pfh_invariant_natural_prefix_body_steps = ff_previous_ph_pfh_invariant_natural_prefix_body_steps * t + ff_coefficient_ph_pfh_invariant_natural_prefix_body_steps)))))) /\ ((n=h*t+a)))))
  46. 0046specialize beta_horner_eval_successor_decompose (b)
  47. 0047specialize beta_horner_eval_successor_decompose (c)
  48. 0048specialize beta_horner_eval_successor_decompose (t)
  49. 0049specialize beta_horner_eval_successor_decompose (l)
  50. 0050specialize beta_horner_eval_successor_decompose (n)
  51. 0051apply beta_horner_eval_successor_decompose
  52. 0052exact hn
  53. 0053cases hns
  54. 0054cases hns_witness
  55. 0055cases hns_witness_witness
  56. 0056cases hns_witness_witness_right
  57. 0057have hrs : exists a h k. ((((exists ff_h_pfp_invariant_canonical_coefficient. ff_h_pfp_invariant_canonical_coefficient + S (a) = S ((S (l)) * e)) /\ exists ff_q_pfp_invariant_canonical_coefficient. d = ff_q_pfp_invariant_canonical_coefficient * S ((S (l)) * e) + (a))) /\ (((exists pfh_trace_code_invariant_canonical_prefix pfh_trace_scale_invariant_canonical_prefix. (((exists pfa_gap_invariant_canonical_prefixtracebase. pfa_gap_invariant_canonical_prefixtracebase + S (t) = (p)) /\ (((((exists ff_h_pfp_invariant_canonical_prefixtraceinitial. ff_h_pfp_invariant_canonical_prefixtraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_invariant_canonical_prefix)) /\ exists ff_q_pfp_invariant_canonical_prefixtraceinitial. pfh_trace_code_invariant_canonical_prefix = ff_q_pfp_invariant_canonical_prefixtraceinitial * S ((S (0)) * pfh_trace_scale_invariant_canonical_prefix) + (0))) /\ (((((exists ff_h_pfp_invariant_canonical_prefixtraceterminal. ff_h_pfp_invariant_canonical_prefixtraceterminal + S (h) = S ((S (l)) * pfh_trace_scale_invariant_canonical_prefix)) /\ exists ff_q_pfp_invariant_canonical_prefixtraceterminal. pfh_trace_code_invariant_canonical_prefix = ff_q_pfp_invariant_canonical_prefixtraceterminal * S ((S (l)) * pfh_trace_scale_invariant_canonical_prefix) + (h))) /\ ((forall pfh_index_invariant_canonical_prefixtracesteps. (exists pfa_gap_invariant_canonical_prefixtracestepsindex. pfa_gap_invariant_canonical_prefixtracestepsindex + S (pfh_index_invariant_canonical_prefixtracesteps) = (l)) -> (exists pfh_coefficient_invariant_canonical_prefixtracestepsstep pfh_before_invariant_canonical_prefixtracestepsstep pfh_after_invariant_canonical_prefixtracestepsstep pfh_product_invariant_canonical_prefixtracestepsstep. ((((exists ff_h_pfp_invariant_canonical_prefixtracestepsstepcoefficient. ff_h_pfp_invariant_canonical_prefixtracestepsstepcoefficient + S (pfh_coefficient_invariant_canonical_prefixtracestepsstep) = S ((S (pfh_index_invariant_canonical_prefixtracesteps)) * e)) /\ exists ff_q_pfp_invariant_canonical_prefixtracestepsstepcoefficient. d = ff_q_pfp_invariant_canonical_prefixtracestepsstepcoefficient * S ((S (pfh_index_invariant_canonical_prefixtracesteps)) * e) + (pfh_coefficient_invariant_canonical_prefixtracestepsstep))) /\ (((((exists ff_h_pfp_invariant_canonical_prefixtracestepsstepbefore. ff_h_pfp_invariant_canonical_prefixtracestepsstepbefore + S (pfh_before_invariant_canonical_prefixtracestepsstep) = S ((S (pfh_index_invariant_canonical_prefixtracesteps)) * pfh_trace_scale_invariant_canonical_prefix)) /\ exists ff_q_pfp_invariant_canonical_prefixtracestepsstepbefore. pfh_trace_code_invariant_canonical_prefix = ff_q_pfp_invariant_canonical_prefixtracestepsstepbefore * S ((S (pfh_index_invariant_canonical_prefixtracesteps)) * pfh_trace_scale_invariant_canonical_prefix) + (pfh_before_invariant_canonical_prefixtracestepsstep))) /\ (((((exists ff_h_pfp_invariant_canonical_prefixtracestepsstepafter. ff_h_pfp_invariant_canonical_prefixtracestepsstepafter + S (pfh_after_invariant_canonical_prefixtracestepsstep) = S ((S (S (pfh_index_invariant_canonical_prefixtracesteps))) * pfh_trace_scale_invariant_canonical_prefix)) /\ exists ff_q_pfp_invariant_canonical_prefixtracestepsstepafter. pfh_trace_code_invariant_canonical_prefix = ff_q_pfp_invariant_canonical_prefixtracestepsstepafter * S ((S (S (pfh_index_invariant_canonical_prefixtracesteps))) * pfh_trace_scale_invariant_canonical_prefix) + (pfh_after_invariant_canonical_prefixtracestepsstep))) /\ (((((exists pfa_gap_invariant_canonical_prefixtracestepsstepmultiplyleft. pfa_gap_invariant_canonical_prefixtracestepsstepmultiplyleft + S (pfh_before_invariant_canonical_prefixtracestepsstep) = (p)) /\ (((exists pfa_gap_invariant_canonical_prefixtracestepsstepmultiplyright. pfa_gap_invariant_canonical_prefixtracestepsstepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_invariant_canonical_prefixtracestepsstepmultiplyresultbound. pfa_gap_invariant_canonical_prefixtracestepsstepmultiplyresultbound + S (pfh_product_invariant_canonical_prefixtracestepsstep) = (p)) /\ ((exists pfa_offset_left_invariant_canonical_prefixtracestepsstepmultiplyresultcongruence pfa_offset_right_invariant_canonical_prefixtracestepsstepmultiplyresultcongruence. ((pfh_before_invariant_canonical_prefixtracestepsstep) * (t)) + (p) * pfa_offset_left_invariant_canonical_prefixtracestepsstepmultiplyresultcongruence = (pfh_product_invariant_canonical_prefixtracestepsstep) + (p) * pfa_offset_right_invariant_canonical_prefixtracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_invariant_canonical_prefixtracestepsstepaddleft. pfa_gap_invariant_canonical_prefixtracestepsstepaddleft + S (pfh_product_invariant_canonical_prefixtracestepsstep) = (p)) /\ (((exists pfa_gap_invariant_canonical_prefixtracestepsstepaddright. pfa_gap_invariant_canonical_prefixtracestepsstepaddright + S (pfh_coefficient_invariant_canonical_prefixtracestepsstep) = (p)) /\ ((((exists pfa_gap_invariant_canonical_prefixtracestepsstepaddresultbound. pfa_gap_invariant_canonical_prefixtracestepsstepaddresultbound + S (pfh_after_invariant_canonical_prefixtracestepsstep) = (p)) /\ ((exists pfa_offset_left_invariant_canonical_prefixtracestepsstepaddresultcongruence pfa_offset_right_invariant_canonical_prefixtracestepsstepaddresultcongruence. ((pfh_product_invariant_canonical_prefixtracestepsstep) + (pfh_coefficient_invariant_canonical_prefixtracestepsstep)) + (p) * pfa_offset_left_invariant_canonical_prefixtracestepsstepaddresultcongruence = (pfh_after_invariant_canonical_prefixtracestepsstep) + (p) * pfa_offset_right_invariant_canonical_prefixtracestepsstepaddresultcongruence))))))))))))))))))))))))))) /\ (((((exists pfa_gap_invariant_canonical_multiplyleft. pfa_gap_invariant_canonical_multiplyleft + S (h) = (p)) /\ (((exists pfa_gap_invariant_canonical_multiplyright. pfa_gap_invariant_canonical_multiplyright + S (t) = (p)) /\ ((((exists pfa_gap_invariant_canonical_multiplyresultbound. pfa_gap_invariant_canonical_multiplyresultbound + S (k) = (p)) /\ ((exists pfa_offset_left_invariant_canonical_multiplyresultcongruence pfa_offset_right_invariant_canonical_multiplyresultcongruence. ((h) * (t)) + (p) * pfa_offset_left_invariant_canonical_multiplyresultcongruence = (k) + (p) * pfa_offset_right_invariant_canonical_multiplyresultcongruence))))))))) /\ ((((exists pfa_gap_invariant_canonical_addleft. pfa_gap_invariant_canonical_addleft + S (k) = (p)) /\ (((exists pfa_gap_invariant_canonical_addright. pfa_gap_invariant_canonical_addright + S (a) = (p)) /\ ((((exists pfa_gap_invariant_canonical_addresultbound. pfa_gap_invariant_canonical_addresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_invariant_canonical_addresultcongruence pfa_offset_right_invariant_canonical_addresultcongruence. ((k) + (a)) + (p) * pfa_offset_left_invariant_canonical_addresultcongruence = (r) + (p) * pfa_offset_right_invariant_canonical_addresultcongruence)))))))))))))))
  58. 0058specialize prime_field_polynomial_horner_successor_decompose (p)
  59. 0059specialize prime_field_polynomial_horner_successor_decompose (d)
  60. 0060specialize prime_field_polynomial_horner_successor_decompose (e)
  61. 0061specialize prime_field_polynomial_horner_successor_decompose (t)
  62. 0062specialize prime_field_polynomial_horner_successor_decompose (l)
  63. 0063specialize prime_field_polynomial_horner_successor_decompose (r)
  64. 0064apply prime_field_polynomial_horner_successor_decompose
  65. 0065exact hr
  66. 0066cases hrs
  67. 0067cases hrs_witness
  68. 0068cases hrs_witness_witness
  69. 0069cases hrs_witness_witness_witness
  70. 0070cases hrs_witness_witness_witness_right
  71. 0071cases hrs_witness_witness_witness_right_right
  72. 0072have hcoefficient : ((exists pfa_gap_invariant_coefficient_residuebound. pfa_gap_invariant_coefficient_residuebound + S (x2) = (p)) /\ ((exists pfa_offset_left_invariant_coefficient_residuecongruence pfa_offset_right_invariant_coefficient_residuecongruence. (x) + (p) * pfa_offset_left_invariant_coefficient_residuecongruence = (x2) + (p) * pfa_offset_right_invariant_coefficient_residuecongruence)))
  73. 0073specialize prime_field_polynomial_normalization_entry (p)
  74. 0074specialize prime_field_polynomial_normalization_entry (b)
  75. 0075specialize prime_field_polynomial_normalization_entry (c)
  76. 0076specialize prime_field_polynomial_normalization_entry (d)
  77. 0077specialize prime_field_polynomial_normalization_entry (e)
  78. 0078specialize prime_field_polynomial_normalization_entry (S l)
  79. 0079specialize prime_field_polynomial_normalization_entry (l)
  80. 0080specialize prime_field_polynomial_normalization_entry (x)
  81. 0081specialize prime_field_polynomial_normalization_entry (x2)
  82. 0082apply prime_field_polynomial_normalization_entry
  83. 0083exact hred
  84. 0084exists 0
  85. 0085apply zero_add
  86. 0086exact hns_witness_witness_left
  87. 0087exact hrs_witness_witness_witness_left
  88. 0088have hprevious : ((exists pfa_gap_invariant_previous_residuebound. pfa_gap_invariant_previous_residuebound + S (x3) = (p)) /\ ((exists pfa_offset_left_invariant_previous_residuecongruence pfa_offset_right_invariant_previous_residuecongruence. (x1) + (p) * pfa_offset_left_invariant_previous_residuecongruence = (x3) + (p) * pfa_offset_right_invariant_previous_residuecongruence)))
  89. 0089specialize IH (x1)
  90. 0090specialize IH (x3)
  91. 0091apply IH
  92. 0092exact hp
  93. 0093intro i
  94. 0094intro hi
  95. 0095specialize hred (i)
  96. 0096apply hred
  97. 0097specialize le_succ (S i)
  98. 0098specialize le_succ (l)
  99. 0099apply le_succ
  100. 0100exact hi
  101. 0101exact hns_witness_witness_right_left
  102. 0102exact hrs_witness_witness_witness_right_left
  103. 0103have hbounds : ((exists pfa_gap_invariant_base_bound. pfa_gap_invariant_base_bound + S (t) = (p)) /\ ((forall fom_index_pfp_invariant_coefficients. (exists fom_gap_pfp_invariant_coefficients_index_bound. fom_gap_pfp_invariant_coefficients_index_bound + S (fom_index_pfp_invariant_coefficients) = l) -> exists fom_value_pfp_invariant_coefficients. ((((exists fom_beta_height_pfp_invariant_coefficients_entry. fom_beta_height_pfp_invariant_coefficients_entry + S (fom_value_pfp_invariant_coefficients) = S ((S (fom_index_pfp_invariant_coefficients)) * e)) /\ exists fom_beta_quotient_pfp_invariant_coefficients_entry. d = fom_beta_quotient_pfp_invariant_coefficients_entry * S ((S (fom_index_pfp_invariant_coefficients)) * e) + (fom_value_pfp_invariant_coefficients))) /\ (exists fom_gap_pfp_invariant_coefficients_value_bound. fom_gap_pfp_invariant_coefficients_value_bound + S (fom_value_pfp_invariant_coefficients) = p)))))
  104. 0104specialize prime_field_polynomial_horner_input_bounds (p)
  105. 0105specialize prime_field_polynomial_horner_input_bounds (d)
  106. 0106specialize prime_field_polynomial_horner_input_bounds (e)
  107. 0107specialize prime_field_polynomial_horner_input_bounds (t)
  108. 0108specialize prime_field_polynomial_horner_input_bounds (l)
  109. 0109specialize prime_field_polynomial_horner_input_bounds (x3)
  110. 0110apply prime_field_polynomial_horner_input_bounds
  111. 0111exact hrs_witness_witness_witness_right_left
  112. 0112cases hbounds
  113. 0113have hproduct : ((exists pfa_gap_invariant_product_residuebound. pfa_gap_invariant_product_residuebound + S (x4) = (p)) /\ ((exists pfa_offset_left_invariant_product_residuecongruence pfa_offset_right_invariant_product_residuecongruence. (x1*t) + (p) * pfa_offset_left_invariant_product_residuecongruence = (x4) + (p) * pfa_offset_right_invariant_product_residuecongruence)))
  114. 0114specialize prime_field_residue_multiply (p)
  115. 0115specialize prime_field_residue_multiply (x1)
  116. 0116specialize prime_field_residue_multiply (t)
  117. 0117specialize prime_field_residue_multiply (x3)
  118. 0118specialize prime_field_residue_multiply (t)
  119. 0119specialize prime_field_residue_multiply (x4)
  120. 0120apply prime_field_residue_multiply
  121. 0121exact hprevious
  122. 0122specialize prime_field_residue_reflexive (p)
  123. 0123specialize prime_field_residue_reflexive (t)
  124. 0124apply prime_field_residue_reflexive
  125. 0125exact hbounds_left
  126. 0126exact hrs_witness_witness_witness_right_right_left
  127. 0127specialize prime_field_residue_input_equal (p)
  128. 0128specialize prime_field_residue_input_equal (n)
  129. 0129specialize prime_field_residue_input_equal (x1*t+x)
  130. 0130specialize prime_field_residue_input_equal (r)
  131. 0131apply prime_field_residue_input_equal
  132. 0132exact hns_witness_witness_right_right
  133. 0133specialize prime_field_residue_add (p)
  134. 0134specialize prime_field_residue_add (x1*t)
  135. 0135specialize prime_field_residue_add (x)
  136. 0136specialize prime_field_residue_add (x4)
  137. 0137specialize prime_field_residue_add (x2)
  138. 0138specialize prime_field_residue_add (r)
  139. 0139apply prime_field_residue_add
  140. 0140exact hproduct
  141. 0141exact hcoefficient
  142. 0142exact hrs_witness_witness_witness_right_right_right