asl zarb
unknown
plain_text
a year ago
5.0 kB
2
Indexable
Never
Goal (|{l | |l| = 4 ∧ (∀ x, x in l -> 0 ≤ x ∧ x < 10) ∧ ~ head 0 l = 0 }| = 9 * 10 * 10 * 10); Proof; replace #1 ({ l: list ℤ | |l| = 4 ∧ (∀ x: ℤ, x in l → 0 ≤ x ∧ x < 10) ∧ ~ head 0 l = 0 }) with ({ l: list ℤ | ∃ a b c d: ℤ, l = [a, b, c, d] ∧ (∀ x: ℤ, x in l → 0 ≤ x ∧ x < 10) ∧ ~ a = 0 }); apply set_from_func_eq; intros; apply and_intro; intros; destruct H with (ex_ind ? ?) to (a a_property); destruct a_property with (ex_ind ? ?) to (b b_property); destruct b_property with (ex_ind ? ?) to (c c_property); destruct c_property with (ex_ind ? ?) to (d d_property); destruct d_property with (and_ind ? ?) to (d_property_l d_property_r); z3; intros; apply (ex_intro ? ? (nth 0 x 0)); apply (ex_intro ? ? (nth 0 x 1)); apply (ex_intro ? ? (nth 0 x 2)); apply (ex_intro ? ? (nth 0 x 3)); z3; apply eq_sym ; replace #1 (9 * 10 * 10 * 10) with (10 * 10 * 10 * 9); lia; apply eq_sym ; apply (asl_zarb3 ?0 ?2 ?4 ?6 ?8 (λ a: ℤ, λ l: list ℤ, ∃ b c d: ℤ, l = [a, b, c, d] ∧ (∀ x: ℤ, x in l → 0 ≤ x ∧ x < 10) ∧ ~ a = 0) (λ x: ℤ, 0 < x ∧ x < 10) ?24 ?26 ?28 ?30); intros; destruct H with (ex_ind ? ?) to (l l_property); destruct l_property with (ex_ind ? ?) to (l_property_value l_property_proof) ; destruct l_property_proof with (ex_ind ? ?) to (l_property_proof_value l_property_proof_proof) ; destruct l_property_proof_proof with (ex_ind ? ?) to (l_property_proof_proof_value l_property_proof_proof_proof) ; destruct l_property_proof_proof_proof with (and_ind ? ?) to (l_property_proof_proof_proof_l l_property_proof_proof_proof_r) ; destruct l_property_proof_proof_proof_r with (and_ind ? ?) to (l_property_proof_proof_proof_r_l l_property_proof_proof_proof_r_r) ; add_hyp l_property_proof_proof_proof_r_l_ex := (l_property_proof_proof_proof_r_l (a)); z3; intros; destruct H0 with (ex_ind ? ?) to (H0_value H0_proof) ; destruct H1 with (ex_ind ? ?) to (H1_value H1_proof) ; destruct H0_proof with (ex_ind ? ?) to (H0_proof_value H0_proof_proof) ; destruct H1_proof with (ex_ind ? ?) to (H1_proof_value H1_proof_proof) ; destruct H0_proof_proof with (ex_ind ? ?) to (H0_proof_proof_value H0_proof_proof_proof) ; destruct H1_proof_proof with (ex_ind ? ?) to (H1_proof_proof_value H1_proof_proof_proof) ; z3; intros; apply (asl_zarb3 ?0 ?2 ?4 ?6 ?8 (λ b: ℤ, λ l: list ℤ, ∃ c d: ℤ, l = [a, b, c, d] ∧ (∀ x: ℤ, x in l → 0 ≤ x ∧ x < 10) ∧ ~ a = 0) (λ b: ℤ, 0 ≤ b ∧ b < 10) ?24 ?26 ?28 ?30); intros; destruct H0 with (ex_ind ? ?) to (H0_value H0_proof) ; destruct H0_proof with (ex_ind ? ?) to (H0_proof_value H0_proof_proof) ; destruct H0_proof_proof with (ex_ind ? ?) to (H0_proof_proof_value H0_proof_proof_proof) ; destruct H0_proof_proof_proof with (and_ind ? ?) to (H0_proof_proof_proof_l H0_proof_proof_proof_r) ; destruct H0_proof_proof_proof_r with (and_ind ? ?) to (H0_proof_proof_proof_r_l H0_proof_proof_proof_r_r) ; add_hyp H0_proof_proof_proof_r_l_ex := (H0_proof_proof_proof_r_l (a0)); z3; intros; destruct H1 with (ex_ind ? ?) to (H1_value H1_proof) ; destruct H2 with (ex_ind ? ?) to (H2_value H2_proof) ; destruct H1_proof with (ex_ind ? ?) to (H1_proof_value H1_proof_proof) ; destruct H2_proof with (ex_ind ? ?) to (H2_proof_value H2_proof_proof) ; z3; intros b; intros; apply (asl_zarb3 ?0 ?2 ?4 ?6 ?8 (λ c: ℤ, λ l: list ℤ, ∃ d: ℤ, l = [a, b, c, d] ∧ (∀ x: ℤ, x in l → 0 ≤ x ∧ x < 10) ∧ ~ a = 0) (λ c: ℤ, 0 ≤ c ∧ c < 10) ?24 ?26 ?28 ?30); intros; destruct H1 with (ex_ind ? ?) to (H1_value H1_proof) ; destruct H1_proof with (ex_ind ? ?) to (H1_proof_value H1_proof_proof) ; destruct H1_proof_proof with (and_ind ? ?) to (H1_proof_proof_l H1_proof_proof_r) ; destruct H1_proof_proof_r with (and_ind ? ?) to (H1_proof_proof_r_l H1_proof_proof_r_r) ; add_hyp H1_proof_proof_r_l_ex := (H1_proof_proof_r_l (a0)); z3; intros; destruct H2 with (ex_ind ? ?) to (H2_value H2_proof) ; destruct H3 with (ex_ind ? ?) to (H3_value H3_proof) ; z3; intros; apply eq_sym ; replace #1 (10) with (1 * 10); lia; apply eq_sym ; apply (asl_zarb3 ?0 ?2 ?4 ?6 ?8 (λ d: ℤ, λ l: list ℤ, l = [a, b, a0, d] ∧ (∀ x: ℤ, x in l → 0 ≤ x ∧ x < 10) ∧ ~ a = 0) (λ d: ℤ, 0 ≤ d ∧ d < 10) ?24 ?26 ?28 ?30); intros; destruct H2 with (ex_ind ? ?) to (H2_value H2_proof) ; destruct H2_proof with (and_ind ? ?) to (H2_proof_l H2_proof_r) ; destruct H2_proof_r with (and_ind ? ?) to (H2_proof_r_l H2_proof_r_r) ; add_hyp H2_proof_r_l_ex := (H2_proof_r_l (a1)); z3; intros; z3; intros; replace #1 ({ l: list ℤ | l = [a, b, a0, a1] ∧ (∀ x: ℤ, x in l → 0 ≤ x ∧ x < 10) ∧ ~ a = 0 }) with ({ [a, b, a0, a1]}); apply set_equality ; apply included_fold ; intros; apply set_from_func_fold ; apply and_intro ; apply and_intro ; lia; intros; z3; auto_set; apply included_fold ; intros; apply set_from_func_unfold in H3 ; auto_set; apply singleton_len ;