Skip to content

Instantly share code, notes, and snippets.

@mukeshtiwari

mukeshtiwari/Rewritefail.v

Last active October 9, 2021 08:43
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save mukeshtiwari/82d56ffdce8e9707cb2c9baf610608b6 to your computer and use it in GitHub Desktop.
Save mukeshtiwari/82d56ffdce8e9707cb2c9baf610608b6 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Rewritefail.v
up: N
Hacc: ∀ y : N, y < up → Acc (λ x y0 : N, x < y0) y
IHup: ∀ y : N, y < up → length (length_byte_list y) = N.to_nat (y / 256 + 1)
Hnp: (up <? 256) = true
Hup: up / 256 = 0
-----------------------------------------------------------------------------
1/1
length
((if up <? 256 as upp return ((up <? 256) = upp → list byte)
then
λ Hnp0 : (up <? 256) = true,
(np_total up (match N.ltb_lt up 256 with
| conj H _ => H
end Hnp0) :: Datatypes.nil)%list
else
λ Hnp0 : (up <? 256) = false,
(np_total (up mod 256) (nmod_256 up)
:: (if up / 256 <? 256 as upp
return ((up / 256 <? 256) = upp → list byte)
then
λ Hnp1 : (up / 256 <? 256) = true,
np_total (up / 256)
(match N.ltb_lt (up / 256) 256 with
| conj H _ => H
end Hnp1) :: Datatypes.nil
else
λ Hnp1 : (up / 256 <? 256) = false,
np_total ((up / 256) mod 256) (nmod_256 (up / 256))
:: (fix length_byte_list
(up0 : N) (H : Acc (λ x y : N, x < y) (up0 / 256))
{struct H} : list byte :=
(if up0 <? 256 as upp
return ((up0 <? 256) = upp → list byte)
then
λ Hnp2 : (up0 <? 256) = true,
np_total up0
(match N.ltb_lt up0 256 with
| conj H0 _ => H0
end Hnp2) :: Datatypes.nil
else
λ Hnp2 : (up0 <? 256) = false,
np_total (up0 mod 256) (nmod_256 up0)
:: length_byte_list (up0 / 256)
(Acc_inv H
match
N_eq_gt up0 (up0 / 256)
(match N.ltb_ge up0 256 with
| conj H0 _ => H0
end Hnp2) eq_refl
with
| conj _ H0 => H0
end)) eq_refl) (up / 256 / 256)
(Acc_ind (λ x : N, ∀ a : N, a < x → Acc N.lt a)
(λ (z : N) (_ : ∀ y : N, zwf y z → Acc zwf y)
(IHz : ∀ y : N,
zwf y z → ∀ a : N, a < y → Acc N.lt a)
(a : N) (Hxa : a < z),
Acc_intro a
(λ (y : N) (Hy : y < a),
IHz a
(Morphisms.iff_flip_impl_subrelation
(N.to_nat a < N.to_nat z)%nat
(Z.of_N a < Z.of_N z)%Z
(ZifyClasses.mkrel nat Z lt Z.of_nat Z.lt
Nat2Z.inj_lt
(N.to_nat a)
(Z.of_N a)
(ZifyClasses.mkapp N nat Z Z N.to_nat
Z.of_N Z.of_nat
(λ x : Z, x) N_nat_Z a
(Z.of_N a) eq_refl)
(N.to_nat z)
(Z.of_N z)
(ZifyClasses.mkapp N nat Z Z N.to_nat
Z.of_N Z.of_nat
(λ x : Z, x) N_nat_Z z
(Z.of_N z) eq_refl))
(ZMicromega.ZTautoChecker_sound
(Tauto.IMPL
(Tauto.A Tauto.isProp
{|
RingMicromega.Flhs :=
EnvRing.PEX 1;
RingMicromega.Fop :=
RingMicromega.OpLt;
RingMicromega.Frhs :=
EnvRing.PEX 2
|} tt) None
(Tauto.A Tauto.isProp
{|
RingMicromega.Flhs :=
EnvRing.PEX 1;
RingMicromega.Fop :=
RingMicromega.OpLt;
RingMicromega.Frhs :=
EnvRing.PEX 2
|} tt)) Datatypes.nil eq_refl
(λ p : positive,
match p with
| (_~1)%positive => 0%Z
| (_~0)%positive => Z.of_N z
| 1%positive => Z.of_N a
end)
(ZifyClasses.rew_iff
(a < z)
(Z.of_N a < Z.of_N z)%Z
(ZifyClasses.mkrel N Z N.lt Z.of_N
Z.lt N2Z.inj_lt a
(Z.of_N a) eq_refl z
(Z.of_N z) eq_refl) Hxa))) y
(Morphisms.iff_flip_impl_subrelation
(y < a) (Z.of_N y < Z.of_N a)%Z
(ZifyClasses.mkrel N Z N.lt Z.of_N Z.lt
N2Z.inj_lt y
(Z.of_N y) eq_refl a
(Z.of_N a) eq_refl)
(ZMicromega.ZTautoChecker_sound
(Tauto.IMPL
(Tauto.A Tauto.isProp
{|
RingMicromega.Flhs :=
EnvRing.PEX 1;
RingMicromega.Fop :=
RingMicromega.OpLt;
RingMicromega.Frhs :=
EnvRing.PEX 2
|} tt) None
(Tauto.A Tauto.isProp
{|
RingMicromega.Flhs :=
EnvRing.PEX 1;
RingMicromega.Fop :=
RingMicromega.OpLt;
RingMicromega.Frhs :=
EnvRing.PEX 2
|} tt)) Datatypes.nil eq_refl
(λ p : positive,
match p with
| (_~1)%positive => 0%Z
| (_~0)%positive => Z.of_N a
| 1%positive => Z.of_N y
end)
(ZifyClasses.rew_iff
(y < a)
(Z.of_N y < Z.of_N a)%Z
(ZifyClasses.mkrel N Z N.lt Z.of_N
Z.lt N2Z.inj_lt y
(Z.of_N y) eq_refl a
(Z.of_N a) eq_refl) Hy)))))
(nat_ind
(λ n : nat,
∀ a : N,
(N.to_nat a < n)%nat
→ Acc (ltof N (λ a0 : N, N.to_nat a0)) a)
(λ (a : N) (Ha : (N.to_nat a < 0)%nat),
False_ind
(Acc (ltof N (λ a0 : N, N.to_nat a0)) a)
(Nat.nlt_0_r Ha))
(λ (n : nat) (IHn : ∀ a : N,
(N.to_nat a < n)%nat
→
Acc
(ltof N
(λ a0 : N, N.to_nat a0)) a)
(a : N) (Ha : (N.to_nat a < S n)%nat),
Acc_intro a
(λ (b : N) (Hb : (N.to_nat b < N.to_nat a)%nat),
IHn b (Nat.lt_le_trans Hb (lt_n_Sm_le Ha))))
(N.to_nat (up / 256)) (up / 256 / 256)
(Nat.lt_le_trans
(Morphisms.iff_flip_impl_subrelation
(N.to_nat (up / 256 / 256) <
N.to_nat (up / 256))%nat
(Z.of_N (up / 256 / 256) < Z.of_N (up / 256))%Z
(ZifyClasses.mkrel nat Z lt Z.of_nat Z.lt
Nat2Z.inj_lt (N.to_nat (up / 256 / 256))
(Z.of_N (up / 256 / 256))
(ZifyClasses.mkapp N nat Z Z N.to_nat
Z.of_N Z.of_nat
(λ x : Z, x) N_nat_Z
(up / 256 / 256)
(Z.of_N (up / 256 / 256)) eq_refl)
(N.to_nat (up / 256))
(Z.of_N (up / 256))
(ZifyClasses.mkapp N nat Z Z N.to_nat
Z.of_N Z.of_nat
(λ x : Z, x) N_nat_Z
(up / 256) (Z.of_N (up / 256)) eq_refl))
(ZMicromega.ZTautoChecker_sound
(Tauto.IMPL
(Tauto.A Tauto.isProp
{|
RingMicromega.Flhs :=
EnvRing.PEX 1;
RingMicromega.Fop :=
RingMicromega.OpLt;
RingMicromega.Frhs :=
EnvRing.PEX 2
|} tt) None
(Tauto.A Tauto.isProp
{|
RingMicromega.Flhs :=
EnvRing.PEX 1;
RingMicromega.Fop :=
RingMicromega.OpLt;
RingMicromega.Frhs :=
EnvRing.PEX 2
|} tt)) Datatypes.nil eq_refl
(λ p : positive,
match p with
| (_~1)%positive => 0%Z
| (_~0)%positive => Z.of_N (up / 256)
| 1%positive => Z.of_N (up / 256 / 256)
end)
(ZifyClasses.rew_iff
(up / 256 / 256 < up / 256)
(Z.of_N (up / 256 / 256) <
Z.of_N (up / 256))%Z
(ZifyClasses.mkrel N Z N.lt Z.of_N Z.lt
N2Z.inj_lt
(up / 256 / 256)
(Z.of_N (up / 256 / 256)) eq_refl
(up / 256)
(Z.of_N (up / 256)) eq_refl)
match
N_eq_gt up
(up / 256)
(match N.ltb_ge up 256 with
| conj H _ => H
end Hnp0) eq_refl
with
| conj _ H => H
end)))
(lt_n_Sm_le (le_n (S (N.to_nat (up / 256)))))))
(up / 256 / 256 / 256)
(Morphisms.iff_flip_impl_subrelation
(up / 256 / 256 / 256 < up / 256 / 256)
(Z.of_N (up / 256 / 256 / 256) <
Z.of_N (up / 256 / 256))%Z
(ZifyClasses.mkrel N Z N.lt Z.of_N Z.lt N2Z.inj_lt
(up / 256 / 256 / 256)
(Z.of_N (up / 256 / 256 / 256)) eq_refl
(up / 256 / 256) (Z.of_N (up / 256 / 256))
eq_refl)
(ZMicromega.ZTautoChecker_sound
(Tauto.IMPL
(Tauto.A Tauto.isProp
{|
RingMicromega.Flhs := EnvRing.PEX 1;
RingMicromega.Fop := RingMicromega.OpLt;
RingMicromega.Frhs := EnvRing.PEX 2
|} tt) None
(Tauto.A Tauto.isProp
{|
RingMicromega.Flhs := EnvRing.PEX 1;
RingMicromega.Fop := RingMicromega.OpLt;
RingMicromega.Frhs := EnvRing.PEX 2
|} tt)) Datatypes.nil eq_refl
(λ p : positive,
match p with
| (_~1)%positive => 0%Z
| (_~0)%positive => Z.of_N (up / 256 / 256)
| 1%positive => Z.of_N (up / 256 / 256 / 256)
end)
(ZifyClasses.rew_iff
(up / 256 / 256 / 256 < up / 256 / 256)
(Z.of_N (up / 256 / 256 / 256) <
Z.of_N (up / 256 / 256))%Z
(ZifyClasses.mkrel N Z N.lt Z.of_N Z.lt
N2Z.inj_lt (up / 256 / 256 / 256)
(Z.of_N (up / 256 / 256 / 256)) eq_refl
(up / 256 / 256)
(Z.of_N (up / 256 / 256)) eq_refl)
match
N_eq_gt (up / 256)
(up / 256 / 256)
(match N.ltb_ge (up / 256) 256 with
| conj H _ => H
end Hnp1) eq_refl
with
| conj _ H => H
end))))) eq_refl)%list) eq_refl) =
Pos.to_nat 1
Error:
Abstracting over the term "up <? 256" leads to a term
λ b : bool,
length
((if b as upp return (b = upp → list byte)
then
λ Hnp0 : b = true,
(np_total up (match N.ltb_lt up 256 with
| conj H _ => H
end Hnp0) :: Datatypes.nil)%list
else
λ Hnp0 : b = false,
(np_total (up mod 256) (nmod_256 up)
:: (if up / 256 <? 256 as upp
return ((up / 256 <? 256) = upp → list byte)
then
λ Hnp1 : (up / 256 <? 256) = true,
np_total (up / 256)
(match N.ltb_lt (up / 256) 256 with
| conj H _ => H
end Hnp1) :: Datatypes.nil
else
λ Hnp1 : (up / 256 <? 256) = false,
np_total ((up / 256) mod 256) (nmod_256 (up / 256))
:: (fix length_byte_list
(up0 : N) (H : Acc (λ x y : N, x < y) (up0 / 256))
{struct H} : list byte :=
(if up0 <? 256 as upp
return ((up0 <? 256) = upp → list byte)
then
λ Hnp2 : (up0 <? 256) = true,
np_total up0
(match N.ltb_lt up0 256 with
| conj H0 _ => H0
end Hnp2) :: Datatypes.nil
else
λ Hnp2 : (up0 <? 256) = false,
np_total (up0 mod 256) (nmod_256 up0)
:: length_byte_list (up0 / 256)
(Acc_inv H
match
N_eq_gt up0 (up0 / 256)
(match N.ltb_ge up0 256 with
| conj H0 _ => H0
end Hnp2) eq_refl
with
| conj _ H0 => H0
end)) eq_refl)
(up / 256 / 256)
(Acc_ind (λ x : N, ∀ a : N, a < x → Acc N.lt a)
(λ (z : N) (_ : ∀ y : N, zwf y z → Acc zwf y)
(IHz : ∀ y : N,
zwf y z → ∀ a : N, a < y → Acc N.lt a)
(a : N) (Hxa : a < z),
Acc_intro a
(λ (y : N) (Hy : y < a),
IHz a
(Morphisms.iff_flip_impl_subrelation
(N.to_nat a < N.to_nat z)%nat
(Z.of_N a < Z.of_N z)%Z
(ZifyClasses.mkrel nat Z lt Z.of_nat
Z.lt Nat2Z.inj_lt
(N.to_nat a)
(Z.of_N a)
(ZifyClasses.mkapp N nat Z Z
N.to_nat Z.of_N Z.of_nat
(λ x : Z, x) N_nat_Z a
(Z.of_N a) eq_refl)
(N.to_nat z)
(Z.of_N z)
(ZifyClasses.mkapp N nat Z Z
N.to_nat Z.of_N Z.of_nat
(λ x : Z, x) N_nat_Z z
(Z.of_N z) eq_refl))
(ZMicromega.ZTautoChecker_sound
(Tauto.IMPL
(Tauto.A Tauto.isProp
{|
RingMicromega.Flhs :=
EnvRing.PEX 1;
RingMicromega.Fop :=
RingMicromega.OpLt;
RingMicromega.Frhs :=
EnvRing.PEX 2
|} tt) None
(Tauto.A Tauto.isProp
{|
RingMicromega.Flhs :=
EnvRing.PEX 1;
RingMicromega.Fop :=
RingMicromega.OpLt;
RingMicromega.Frhs :=
EnvRing.PEX 2
|} tt)) Datatypes.nil eq_refl
(λ p : positive,
match p with
| (_~1)%positive => 0%Z
| (_~0)%positive => Z.of_N z
| 1%positive => Z.of_N a
end)
(ZifyClasses.rew_iff
(a < z)
(Z.of_N a < Z.of_N z)%Z
(ZifyClasses.mkrel N Z N.lt
Z.of_N Z.lt N2Z.inj_lt a
(Z.of_N a) eq_refl z
(Z.of_N z) eq_refl) Hxa))) y
(Morphisms.iff_flip_impl_subrelation
(y < a) (Z.of_N y < Z.of_N a)%Z
(ZifyClasses.mkrel N Z N.lt Z.of_N Z.lt
N2Z.inj_lt y
(Z.of_N y) eq_refl a
(Z.of_N a) eq_refl)
(ZMicromega.ZTautoChecker_sound
(Tauto.IMPL
(Tauto.A Tauto.isProp
{|
RingMicromega.Flhs :=
EnvRing.PEX 1;
RingMicromega.Fop :=
RingMicromega.OpLt;
RingMicromega.Frhs :=
EnvRing.PEX 2
|} tt) None
(Tauto.A Tauto.isProp
{|
RingMicromega.Flhs :=
EnvRing.PEX 1;
RingMicromega.Fop :=
RingMicromega.OpLt;
RingMicromega.Frhs :=
EnvRing.PEX 2
|} tt)) Datatypes.nil eq_refl
(λ p : positive,
match p with
| (_~1)%positive => 0%Z
| (_~0)%positive => Z.of_N a
| 1%positive => Z.of_N y
end)
(ZifyClasses.rew_iff
(y < a)
(Z.of_N y < Z.of_N a)%Z
(ZifyClasses.mkrel N Z N.lt
Z.of_N Z.lt N2Z.inj_lt y
(Z.of_N y) eq_refl a
(Z.of_N a) eq_refl) Hy)))))
(nat_ind
(λ n : nat,
∀ a : N,
(N.to_nat a < n)%nat
→ Acc (ltof N (λ a0 : N, N.to_nat a0)) a)
(λ (a : N) (Ha : (N.to_nat a < 0)%nat),
False_ind
(Acc (ltof N (λ a0 : N, N.to_nat a0)) a)
(Nat.nlt_0_r Ha))
(λ (n : nat) (IHn : ∀ a : N,
(N.to_nat a < n)%nat
→
Acc
(ltof N
(λ a0 : N, N.to_nat a0)) a)
(a : N) (Ha : (N.to_nat a < S n)%nat),
Acc_intro a
(λ (b0 : N) (Hb :
(N.to_nat b0 < N.to_nat a)%nat),
IHn b0
(Nat.lt_le_trans Hb (lt_n_Sm_le Ha))))
(N.to_nat (up / 256))
(up / 256 / 256)
(Nat.lt_le_trans
(Morphisms.iff_flip_impl_subrelation
(N.to_nat (up / 256 / 256) <
N.to_nat (up / 256))%nat
(Z.of_N (up / 256 / 256) <
Z.of_N (up / 256))%Z
(ZifyClasses.mkrel nat Z lt Z.of_nat Z.lt
Nat2Z.inj_lt
(N.to_nat (up / 256 / 256))
(Z.of_N (up / 256 / 256))
(ZifyClasses.mkapp N nat Z Z N.to_nat
Z.of_N Z.of_nat
(λ x : Z, x) N_nat_Z
(up / 256 / 256)
(Z.of_N (up / 256 / 256)) eq_refl)
(N.to_nat (up / 256))
(Z.of_N (up / 256))
(ZifyClasses.mkapp N nat Z Z N.to_nat
Z.of_N Z.of_nat
(λ x : Z, x) N_nat_Z
(up / 256)
(Z.of_N (up / 256)) eq_refl))
(ZMicromega.ZTautoChecker_sound
(Tauto.IMPL
(Tauto.A Tauto.isProp
{|
RingMicromega.Flhs :=
EnvRing.PEX 1;
RingMicromega.Fop :=
RingMicromega.OpLt;
RingMicromega.Frhs :=
EnvRing.PEX 2
|} tt) None
(Tauto.A Tauto.isProp
{|
RingMicromega.Flhs :=
EnvRing.PEX 1;
RingMicromega.Fop :=
RingMicromega.OpLt;
RingMicromega.Frhs :=
EnvRing.PEX 2
|} tt)) Datatypes.nil eq_refl
(λ p : positive,
match p with
| (_~1)%positive => 0%Z
| (_~0)%positive => Z.of_N (up / 256)
| 1%positive =>
Z.of_N (up / 256 / 256)
end)
(ZifyClasses.rew_iff
(up / 256 / 256 < up / 256)
(Z.of_N (up / 256 / 256) <
Z.of_N (up / 256))%Z
(ZifyClasses.mkrel N Z N.lt Z.of_N
Z.lt N2Z.inj_lt
(up / 256 / 256)
(Z.of_N (up / 256 / 256)) eq_refl
(up / 256)
(Z.of_N (up / 256)) eq_refl)
match
N_eq_gt up
(up / 256)
(match N.ltb_ge up 256 with
| conj H _ => H
end Hnp0) eq_refl
with
| conj _ H => H
end)))
(lt_n_Sm_le (le_n (S (N.to_nat (up / 256)))))))
(up / 256 / 256 / 256)
(Morphisms.iff_flip_impl_subrelation
(up / 256 / 256 / 256 < up / 256 / 256)
(Z.of_N (up / 256 / 256 / 256) <
Z.of_N (up / 256 / 256))%Z
(ZifyClasses.mkrel N Z N.lt Z.of_N Z.lt
N2Z.inj_lt (up / 256 / 256 / 256)
(Z.of_N (up / 256 / 256 / 256)) eq_refl
(up / 256 / 256) (Z.of_N (up / 256 / 256))
eq_refl)
(ZMicromega.ZTautoChecker_sound
(Tauto.IMPL
(Tauto.A Tauto.isProp
{|
RingMicromega.Flhs := EnvRing.PEX 1;
RingMicromega.Fop :=
RingMicromega.OpLt;
RingMicromega.Frhs := EnvRing.PEX 2
|} tt) None
(Tauto.A Tauto.isProp
{|
RingMicromega.Flhs := EnvRing.PEX 1;
RingMicromega.Fop :=
RingMicromega.OpLt;
RingMicromega.Frhs := EnvRing.PEX 2
|} tt)) Datatypes.nil eq_refl
(λ p : positive,
match p with
| (_~1)%positive => 0%Z
| (_~0)%positive => Z.of_N (up / 256 / 256)
| 1%positive =>
Z.of_N (up / 256 / 256 / 256)
end)
(ZifyClasses.rew_iff
(up / 256 / 256 / 256 < up / 256 / 256)
(Z.of_N (up / 256 / 256 / 256) <
Z.of_N (up / 256 / 256))%Z
(ZifyClasses.mkrel N Z N.lt Z.of_N Z.lt
N2Z.inj_lt (up / 256 / 256 / 256)
(Z.of_N (up / 256 / 256 / 256)) eq_refl
(up / 256 / 256)
(Z.of_N (up / 256 / 256)) eq_refl)
match
N_eq_gt (up / 256)
(up / 256 / 256)
(match N.ltb_ge (up / 256) 256 with
| conj H _ => H
end Hnp1) eq_refl
with
| conj _ H => H
end))))) eq_refl)%list) eq_refl) =
Pos.to_nat 1
which is ill-typed.
Reason is: Incorrect elimination of "N.ltb_lt up 256" in the inductive type
"and":
ill-formed elimination predicate.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment