From 2c31f199f35d96d7b0dd86f738c8d4887b37446d Mon Sep 17 00:00:00 2001 From: Matthias Puech Date: Thu, 25 Mar 2010 16:23:10 +0000 Subject: [PATCH] Automation problem From: puech --- .../software/matita/nlibrary/arithmetics/R.ma | 35 ++++++++++++++++--- 1 file changed, 31 insertions(+), 4 deletions(-) diff --git a/helm/software/matita/nlibrary/arithmetics/R.ma b/helm/software/matita/nlibrary/arithmetics/R.ma index f1da6c497..5499311dc 100644 --- a/helm/software/matita/nlibrary/arithmetics/R.ma +++ b/helm/software/matita/nlibrary/arithmetics/R.ma @@ -20,9 +20,11 @@ ncoercion nat_to_Q : ∀x:nat.Q ≝ nat_to_Q on _x:nat to Q. naxiom Qplus: Q → Q → Q. naxiom Qtimes: Q → Q → Q. naxiom Qdivides: Q → Q → Q. +naxiom Qle : Q → Q → Prop. interpretation "Q plus" 'plus x y = (Qplus x y). interpretation "Q times" 'times x y = (Qtimes x y). interpretation "Q divides" 'divide x y = (Qdivides x y). +interpretation "Q le" 'leq x y = (Qle x y). naxiom Qtimes_plus: ∀n,m:nat.∀q:Q. (n * q + m * q) = (plus n m) * q. naxiom Qmult_one: ∀q:Q. 1 * q = q. naxiom Qdivides_mult: ∀q1,q2. (q1 * q2) / q1 = q2. @@ -32,6 +34,8 @@ naxiom Qplus_comm: ∀q1,q2. q1 + q2 = q2 + q1. naxiom Qplus_assoc: ∀q1,q2,q3. q1 + q2 + q3 = q1 + (q2 + q3). ntheorem Qplus_assoc1: ∀q1,q2,q3. q1 + q2 + q3 = q3 + q2 + q1. #a; #b; #c; //; nqed. +naxiom Qle_refl: ∀q1. q1≤q1. +naxiom Qle_trans: transitive ? le. (* naxiom Ndivides_mult: ∀n:nat.∀q. (n * q) / n = q. *) @@ -46,15 +50,32 @@ ndefinition ccc ≝ Qdivides_mult.*) naxiom disjoint: Q → Q → Q → Q → bool. ncoinductive locate : Q → Q → Prop ≝ - L: ∀l,u. locate l ((2 * l + u) / 3) → locate l u - | H: ∀l,u. locate ((l + 2 * u) / 3) u → locate l u. + L: ∀l,l',u',u. l≤l' → u'≤((2 * l + u) / 3) → locate l' u' → locate l u + | H: ∀l,l',u',u. ((l + 2 * u) / 3)≤l' → u'≤ u → locate l' u' → locate l u. + +ndefinition locate_inv_ind ≝ +λx1,x2:Q.λP:Q → Q → Prop. + λH1: ∀l,l',u',u.l≤l' → u'≤((2 * l + u) / 3) → locate l' u' → P l u. + λH2: ∀l,l',u',u. ((l + 2 * u) / 3)≤l' → u'≤ u → locate l' u' → P l u. + λHterm:locate x1 x2. + (λHcut:x1=x1 → x2=x2 → P x1 x2. Hcut (refl Q x1) (refl Q x2)) + match Hterm return λy1,y2.λp:locate y1 y2. + x1=y1 → x2=y2 → P y1 y2 + with + [ L l l' u' u Hle1 Hle2 r ⇒ ?(*H1 l l' u' u ?*) + | H l l' u' u Hle1 Hle2 r ⇒ ?(*H2 l l' u' u ?*)]. + ##[ #a; #b; /2/; napply H2; //; (* Qui non va auto! *) + + napply (H2 … r …); //; + /2/; + #h1; #h2; /2/; napply (H2 l l' u' u); ndefinition R ≝ ∃l,u:Q. locate l u. nlet corec Q_to_locate q : locate q q ≝ L q q ?. ncut (q = (2*q+q)/3) [##2: #H; ncases H; (*NOT WORKING: nrewrite > H;*) napply Q_to_locate - |nrewrite < (Qdivides_mult 3 q) in ⊢ (? ? % ?);// + | nrewrite < (Qdivides_mult 3 q) in ⊢ (? ? % ?);// ] nqed. @@ -67,7 +88,13 @@ nlet corec locate_add (l1,u1:?) (r1: locate l1 u1) (l2,u2:?) (r2: locate l2 u2) ncases r1; ncases r2; #l2; #u2; #r2; #l1; #u1; #r1 [ ##1: @1; napplyS (locate_add … r1 …r2); ##|##4: @2; napplyS (locate_add … r1 …r2); - ##| ncases r2; #l2'; #u2'; #r2'; + ##| ninversion r2; #q; #q0; #H; #K; + ndestruct; #U; nrewrite < U in H ⊢ %; #r2'; + ninversion r1;#q; #q0; #H; #K; + nrewrite < K in H ⊢ %; #H; #J; nrewrite < J in H; + #r1'; + ##[ @; nlapply (locate_add …r1'…r2'); #H; + . nlet corec apart (l1,u1) (r1: locate l1 u1) (l2,u2) (r2: locate l2 u2) : CProp[0] ≝ -- 2.39.2