From 10041c91e21dce61faca9725d7073f7c21762019 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 10 Jan 2019 17:45:47 +0100 Subject: Integer conversion now relies on the injection T2Z and its properties --- src/Conversion_tactics.v | 193 +++++++++++++++++++---------------------------- 1 file changed, 76 insertions(+), 117 deletions(-) diff --git a/src/Conversion_tactics.v b/src/Conversion_tactics.v index 5c4be13..d450e3f 100644 --- a/src/Conversion_tactics.v +++ b/src/Conversion_tactics.v @@ -29,37 +29,32 @@ Axiom T2Z_id : forall x : T, Z2T (T2Z x) = x. Par exemple, pour nat il s'agit de (0 <=? z)%Z *) Parameter inT : Z -> bool. (* L'image de l'injection satisfait cette propriété *) -Axiom T2Z_pres : forall x, inT (T2Z x) = true. +Axiom T2Z_pres : forall x : T, inT (T2Z x) = true. +(* Il est toujours possible de définir inT par Z.eqb z (T2Z (Z2T z))>. + Dans ce cas la preuve de l'axiome ci-dessus est essentiellement : + . *) + +(* On demande que cette injection soit un morphisme pour chacun des symboles suivants *) (* Addition *) Parameter add : T -> T -> T. -(* Pour des éléments venant de T, l'addition commute avec Z2T *) -Axiom add_morph : forall x y, inT x = true -> inT y = true -> add (Z2T x) (Z2T y) = Z2T (Z.add x y). -(* Pour des éléments venant de T, l'addition vient de T *) -Axiom add_pres : forall x y, inT x = true -> inT y = true -> inT (Z.add x y) = true. +Axiom t2z_add_morph : forall x' y', Z.add (T2Z x') (T2Z y') = T2Z (add x' y'). (* Multiplication *) Parameter mul : T -> T -> T. -(* Pour des éléments venant de T, la multiplication commute avec Z2T *) -Axiom mul_morph : forall x y, inT x = true -> inT y = true -> mul (Z2T x) (Z2T y) = Z2T (Z.mul x y). -(* Pour des éléments venant de T, la multiplication vient de T *) -Axiom mul_pres : forall x y, inT x = true -> inT y = true -> inT (Z.mul x y) = true. +Axiom t2z_mul_morph : forall x' y', Z.mul (T2Z x') (T2Z y') = T2Z (mul x' y'). (* <= *) Parameter leb : T -> T -> bool. -(* Pour des éléments venant de T, <= commute avec Z2T *) -Axiom leb_morph : forall x y, inT x = true -> inT y = true -> Z.leb x y = leb (Z2T x) (Z2T y). +Axiom t2z_leb_morph : forall x' y', Z.leb (T2Z x') (T2Z y') = leb x' y'. (* < *) Parameter ltb : T -> T -> bool. -(* Pour des éléments venant de T, < commute avec Z2T *) -Axiom ltb_morph : forall x y, inT x = true -> inT y = true -> Z.ltb x y = ltb (Z2T x) (Z2T y). +Axiom t2z_ltb_morph : forall x' y', Z.ltb (T2Z x') (T2Z y') = ltb x' y'. (* = *) Parameter eqb : T -> T -> bool. -(* Pour des éléments venant de T, = commute avec Z2T *) -Axiom eqb_morph : forall x y, inT x = true -> inT y = true -> Z.eqb x y = eqb (Z2T x) (Z2T y). - +Axiom t2z_eqb_morph : forall x' y', Z.eqb (T2Z x') (T2Z y') = eqb x' y'. End convert_type. (* Ce foncteur construit une tactique de conversion à partir d'un module du type ci-dessus *) @@ -83,10 +78,10 @@ Ltac inverse_tactic tactic := try (tactic; fail 1). (* constr_neq t u échoue si et seulement si t et u sont convertibles *) Ltac constr_neq t u := inverse_tactic ltac:(constr_eq t u). -(* is_not_constructor T sym échoue si et seulement si sym est un symbole de constructeur de U *) -Ltac is_not_constructor T sym := +(* is_not_constructor U sym échoue si et seulement si sym est un symbole de constructeur de U *) +Ltac is_not_constructor U sym := let H := fresh in -assert (T -> True) as H by +assert (U -> True) as H by (let x := fresh in let y := fresh in intro x; @@ -97,10 +92,11 @@ assert (T -> True) as H by constr_neq sym c; exact I); clear H. -(* is_not_constructor U sym réussit si et seulement si sym est un symbole de constructeur de U *) +(* is_constructor U sym réussit si et seulement si sym est un symbole de constructeur de U *) Ltac is_constructor U sym := inverse_tactic ltac:(is_not_constructor U sym). -(* Remplace tous les sous-termes x de type T par Z2T (T2Z p) *) +(* Remplace les sous-termes x de type T qui ne sont pas en-dessous d'un symbole connu + par Z2T (T2Z x) *) Ltac converting := (* Coeur de la tactique *) repeat @@ -114,31 +110,30 @@ Ltac converting := lazymatch x with (* Si x est de la forme Z2T (T2Z _) on abandonne le match car x est déjà réécrit *) | Z2T (T2Z _) => fail - (* Il n'est pas nécessaire de réécrire au dessus des symboles connus *) - | add _ _ => fail - | mul _ _ => fail | _ => (* On crée une variable fraîche de type T *) let var := fresh in pose proof x as var; (* Sinon, on analyse la formule obtenue en remplaçant x par notre variable fraîche dans le but *) lazymatch context C[var] with - (* Si elle contient le terme Z2T (T2Z var), cela signifie que le contexte C[] - est de la forme C'[Z2T (T2Z [])] et donc on abandonne le match car x est déjà réécrit *) - | appcontext [Z2T (T2Z var)] => fail - (* Idem: si le contexte contient un constructeur de Z, c'est qu'on est à l'intérieur d'une constante *) - | appcontext [Zpos var] => fail - | appcontext [Zneg var] => fail | appcontext [?h var] => + let h := get_head h in + lazymatch h with + (* x est déjà réécrit *) + | T2Z => fail + (* Pas nécessaire de réécrire en-dessous des symboles qui commutent avec T2Z *) + | add => fail | mul => fail | ltb => fail | leb => fail | eqb => fail + (* Ne pas réécrire à l'intérieur d'une constante *) + | Zpos => fail | Zneg => fail + | _ => (* Idem: si le contexte contient un constructeur de T et que x commence par un constructeur de T, c'est qu'on est à l'intérieur d'une constante *) - let h := get_head h in let hx := get_head x in try (is_constructor T h; is_constructor T hx; fail 1); (* Sinon, on réécrit *) let old_goal := context C[x] in let new_goal := context C[Z2T (T2Z x)] in - replace old_goal with new_goal by (rewrite (T2Z_id x); reflexivity) + replace old_goal with new_goal by (rewrite (T2Z_id x); reflexivity) end end; (* On efface notre variable fraîche *) clear var @@ -146,19 +141,13 @@ Ltac converting := end end. -(* Résoud les hypothèses inT lors de la réécriture des opérations *) -Ltac solve_inT := repeat (try apply add_pres; try apply mul_pres; try apply T2Z_pres); reflexivity. - -(* Réécrit les opérations et relations de T vers Z *) Ltac rewriting := - repeat - match goal with - | |- context [add (Z2T ?X) (Z2T ?Y)] => replace (add (Z2T X) (Z2T Y)) with (Z2T (X + Y)) by (rewrite add_morph; solve_inT) - | |- context [mul (Z2T ?X) (Z2T ?Y)] => replace (mul (Z2T X) (Z2T Y)) with (Z2T (X * Y)) by (rewrite mul_morph; solve_inT) - | |- context [ltb (Z2T ?X) (Z2T ?Y)] => replace (ltb (Z2T X) (Z2T Y)) with (Z.ltb X Y) by (rewrite ltb_morph; solve_inT) - | |- context [leb (Z2T ?X) (Z2T ?Y)] => replace (leb (Z2T X) (Z2T Y)) with (Z.leb X Y) by (rewrite leb_morph; solve_inT) - | |- context [eqb (Z2T ?X) (Z2T ?Y)] => replace (eqb (Z2T X) (Z2T Y)) with (Z.eqb X Y) by (rewrite eqb_morph; solve_inT) - end. + repeat (try rewrite <- t2z_leb_morph; + try rewrite <- t2z_ltb_morph; + try rewrite <- t2z_eqb_morph; + try rewrite <- t2z_add_morph; + try rewrite <- t2z_mul_morph). + (* expand_type [Tn;...T2;;T1] T = T1->T2->...->Tn->T *) Fixpoint expand_type l T : Type := @@ -236,7 +225,7 @@ Ltac renaming := let args := get_args X' in (* Soit Y = fe_id t'1 ... t'n *) let Y := apply_args fe_id args in - (* Et remplaçons (T2Z (f t'1 ... t'n)) par Y *) + (* Et remplaçons (T2Z (f' t'1 ... t'n)) par Y *) change (T2Z X') with Y end; (* On abstrait sur (fe_id := fun x1 ... xn => T2Z (f x1 ... xn)) *) @@ -296,11 +285,11 @@ Ltac renaming' := let f' := get_head X' in (* Si f' = f *) constr_eq f f'; - (* Soit args = [t'1;...;t'n] *) + (* Soit args = [t'1;...;t'(n-1)] *) let args := get_args X' in - (* Soit Z = (fun x1 ... xn => f x1 ... (Z2T xn)) t'1 ... t'n *) + (* Soit Z = (fun x1 ... xn => f x1 ... (Z2T xn)) t'1 ... t'(n-1) *) let Z := apply_args fe args in - (* Et remplaçons (f t'1 ... (Z2T t'n)) par Z *) + (* Et remplaçons (f' t'1 ... (Z2T t'n)) par (Z t'n) *) change (X' (Z2T Y')) with (Z Y') end; (* On abstrait sur (fun x1 ... xn => (f x1 ... (Z2T xn)) *) @@ -344,29 +333,24 @@ Definition inT : Z -> bool := fun z => Z.ltb 0 z. Lemma T2Z_pres : forall x, inT (T2Z x) = true. reflexivity. Qed. Definition add : T -> T -> T := Pos.add. -Lemma add_morph : forall x y, inT x = true -> inT y = true -> add (Z2T x) (Z2T y) = Z2T (Z.add x y). -intros x y; destruct x, y; try discriminate; reflexivity. Qed. -Lemma add_pres : forall x y, inT x = true -> inT y = true -> inT (Z.add x y) = true. -intros x y; destruct x, y; try discriminate; reflexivity. Qed. +Lemma t2z_add_morph : forall x' y', Z.add (T2Z x') (T2Z y') = T2Z (add x' y'). +Proof. reflexivity. Qed. Definition mul : T -> T -> T := Pos.mul. -Lemma mul_morph : forall x y, inT x = true -> inT y = true -> mul (Z2T x) (Z2T y) = Z2T (Z.mul x y). -intros x y; destruct x, y; try discriminate; reflexivity. Qed. -Lemma mul_pres : forall x y, inT x = true -> inT y = true -> inT (Z.mul x y) = true. -intros x y; destruct x, y; try discriminate; reflexivity. Qed. +Lemma t2z_mul_morph : forall x' y', Z.mul (T2Z x') (T2Z y') = T2Z (mul x' y'). +Proof. reflexivity. Qed. Definition leb : T -> T -> bool := Pos.leb. -Lemma leb_morph : forall x y, inT x = true -> inT y = true -> Z.leb x y = leb (Z2T x) (Z2T y). -intros x y; destruct x, y; try discriminate; reflexivity. Qed. +Lemma t2z_leb_morph : forall x' y', Z.leb (T2Z x') (T2Z y') = leb x' y'. +Proof. reflexivity. Qed. Definition ltb : T -> T -> bool := Pos.ltb. -Lemma ltb_morph : forall x y, inT x = true -> inT y = true -> Z.ltb x y = ltb (Z2T x) (Z2T y). -intros x y; destruct x, y; try discriminate; reflexivity. Qed. +Lemma t2z_ltb_morph : forall x' y', Z.ltb (T2Z x') (T2Z y') = ltb x' y'. +Proof. reflexivity. Qed. Definition eqb : T -> T -> bool := Pos.eqb. -Lemma eqb_morph : forall x y, inT x = true -> inT y = true -> Z.eqb x y = eqb (Z2T x) (Z2T y). -intros x y; destruct x, y; try discriminate; reflexivity. Qed. - +Lemma t2z_eqb_morph : forall x' y', Z.eqb (T2Z x') (T2Z y') = eqb x' y'. +Proof. reflexivity. Qed. End pos_convert_type. Module pos_convert_mod := convert pos_convert_type. @@ -386,28 +370,24 @@ Definition inT : Z -> bool := fun z => Z.leb 0 z. Lemma T2Z_pres : forall x, inT (T2Z x) = true. intro; unfold inT; rewrite Z.leb_le; apply N2Z.is_nonneg. Qed. Definition add : T -> T -> T := N.add. -Lemma add_morph : forall x y, inT x = true -> inT y = true -> add (Z2T x) (Z2T y) = Z2T (Z.add x y). -intros x y; destruct x, y; try discriminate; reflexivity. Qed. -Lemma add_pres : forall x y, inT x = true -> inT y = true -> inT (Z.add x y) = true. -intros x y; destruct x, y; try discriminate; reflexivity. Qed. +Lemma t2z_add_morph : forall x' y', Z.add (T2Z x') (T2Z y') = T2Z (add x' y'). +Proof. intros x y; destruct x, y; reflexivity. Qed. Definition mul : T -> T -> T := N.mul. -Lemma mul_morph : forall x y, inT x = true -> inT y = true -> mul (Z2T x) (Z2T y) = Z2T (Z.mul x y). -intros x y; destruct x, y; try discriminate; reflexivity. Qed. -Lemma mul_pres : forall x y, inT x = true -> inT y = true -> inT (Z.mul x y) = true. -intros x y; destruct x, y; try discriminate; reflexivity. Qed. +Lemma t2z_mul_morph : forall x' y', Z.mul (T2Z x') (T2Z y') = T2Z (mul x' y'). +Proof. intros x y; destruct x, y; reflexivity. Qed. Definition leb : T -> T -> bool := N.leb. -Lemma leb_morph : forall x y, inT x = true -> inT y = true -> Z.leb x y = leb (Z2T x) (Z2T y). -intros x y; destruct x, y; try discriminate; reflexivity. Qed. +Lemma t2z_leb_morph : forall x' y', Z.leb (T2Z x') (T2Z y') = leb x' y'. +Proof. intros x y; destruct x, y; reflexivity. Qed. Definition ltb : T -> T -> bool := N.ltb. -Lemma ltb_morph : forall x y, inT x = true -> inT y = true -> Z.ltb x y = ltb (Z2T x) (Z2T y). -intros x y; destruct x, y; try discriminate; reflexivity. Qed. +Lemma t2z_ltb_morph : forall x' y', Z.ltb (T2Z x') (T2Z y') = ltb x' y'. +Proof. intros x y; destruct x, y; reflexivity. Qed. Definition eqb : T -> T -> bool := N.eqb. -Lemma eqb_morph : forall x y, inT x = true -> inT y = true -> Z.eqb x y = eqb (Z2T x) (Z2T y). -intros x y; destruct x, y; try discriminate; reflexivity. Qed. +Lemma t2z_eqb_morph : forall x' y', Z.eqb (T2Z x') (T2Z y') = eqb x' y'. +Proof. intros x y; destruct x, y; reflexivity. Qed. End N_convert_type. @@ -429,56 +409,35 @@ Definition inT : Z -> bool := fun z => Z.leb 0 z. Lemma T2Z_pres : forall x, inT (T2Z x) = true. intro; unfold inT; rewrite Z.leb_le; apply Nat2Z.is_nonneg. Qed. Definition add : T -> T -> T := Nat.add. -Lemma add_morph : forall x y, inT x = true -> inT y = true -> add (Z2T x) (Z2T y) = Z2T (Z.add x y). -intros x y; destruct x, y; try discriminate; try reflexivity. -intros; apply Nat.add_0_r. -unfold inT; rewrite 2 Z.leb_le. -symmetry; apply Z2Nat.inj_add; assumption. -Qed. -Lemma add_pres : forall x y, inT x = true -> inT y = true -> inT (Z.add x y) = true. -intros x y; destruct x, y; try discriminate; reflexivity. Qed. +Lemma t2z_add_morph : forall x' y', Z.add (T2Z x') (T2Z y') = T2Z (add x' y'). +Proof. symmetry. apply Nat2Z.inj_add. Qed. Definition mul : T -> T -> T := Nat.mul. -Lemma mul_morph : forall x y, inT x = true -> inT y = true -> mul (Z2T x) (Z2T y) = Z2T (Z.mul x y). -intros x y; destruct x, y; try discriminate; try reflexivity. -intros; apply Nat.mul_0_r. -unfold inT; rewrite 2 Z.leb_le. -symmetry; apply Z2Nat.inj_mul; assumption. -Qed. -Lemma mul_pres : forall x y, inT x = true -> inT y = true -> inT (Z.mul x y) = true. -intros x y; destruct x, y; try discriminate; reflexivity. Qed. +Lemma t2z_mul_morph : forall x' y', Z.mul (T2Z x') (T2Z y') = T2Z (mul x' y'). +Proof. symmetry. apply Nat2Z.inj_mul. Qed. Definition leb : T -> T -> bool := Nat.leb. -Lemma leb_morph : forall x y, inT x = true -> inT y = true -> Z.leb x y = leb (Z2T x) (Z2T y). -intros x y; destruct x, y; try discriminate; try reflexivity. -intros H1 H2; clear H1 H2; change (Zpos p <=? 0)%Z with false; unfold Z2T, leb; symmetry. -apply Bool.not_true_is_false; rewrite Nat.leb_le. -apply lt_not_le; apply Pos2Nat.is_pos. -intros H1 H2; unfold Z2T, leb; apply Bool.eq_true_iff_eq. -rewrite Z.leb_le, Nat.leb_le, Z2Nat.inj_le; try reflexivity; apply Zle_0_pos. +Lemma t2z_leb_morph : forall x' y', Z.leb (T2Z x') (T2Z y') = leb x' y'. +Proof. + intros x y; unfold leb. + case_eq (x <=? y); [| rewrite <- 2 Bool.not_true_iff_false]; + rewrite <- Zle_is_le_bool; rewrite Nat.leb_le; rewrite Nat2Z.inj_le; auto. Qed. Definition ltb : T -> T -> bool := Nat.ltb. -Lemma ltb_morph : forall x y, inT x = true -> inT y = true -> Z.ltb x y = ltb (Z2T x) (Z2T y). -intros x y; destruct x, y; try discriminate; try reflexivity. -intros H1 H2; clear H1 H2; change (0 T -> bool := Nat.eqb. -Lemma eqb_morph : forall x y, inT x = true -> inT y = true -> Z.eqb x y = eqb (Z2T x) (Z2T y). -intros x y; destruct x, y; try discriminate; try reflexivity; unfold inT, Z2T, eqb. -intros H1 H2; clear H1 H2; change (0 =? Zpos p)%Z with false; symmetry. -rewrite Nat.eqb_neq, Z2Nat.inj_iff; discriminate. -intros H1 H2; clear H1 H2; change (Zpos p =? 0)%Z with false; symmetry. -rewrite Nat.eqb_neq, Z2Nat.inj_iff; discriminate. -intros H1 H2; clear H1 H2; apply Bool.eq_true_iff_eq. -rewrite Z.eqb_eq, Nat.eqb_eq, Z2Nat.inj_iff; try reflexivity; apply Zle_0_pos. +Lemma t2z_eqb_morph : forall x' y', Z.eqb (T2Z x') (T2Z y') = eqb x' y'. +Proof. + intros x y; unfold eqb. + case_eq (x =? y); [| rewrite <- 2 Bool.not_true_iff_false]; + rewrite Z.eqb_eq; rewrite Nat.eqb_eq; rewrite Nat2Z.inj_iff; auto. Qed. End nat_convert_type. -- cgit