From 708a4d82ee37bcfa3c79eae09e0f8fc5a9892408 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Thu, 20 Feb 2020 17:32:51 +0100
Subject: [PATCH] ok with let encoding
---
sandbox/cert_f/rat.lp | 13 +++++--------
1 file changed, 5 insertions(+), 8 deletions(-)
diff --git a/sandbox/cert_f/rat.lp b/sandbox/cert_f/rat.lp
index 7b27440..0beee59 100644
--- a/sandbox/cert_f/rat.lp
+++ b/sandbox/cert_f/rat.lp
@@ -11,13 +11,13 @@ symbol frac : Term nat ⇒ Term N.nznat ⇒ Term rat
symbol times : @Term Type rat ⇒ @Term Type rat ⇒ @Term Type rat
rule times (frac &a &b) (frac &c &d) →
+ let bv ≔ fst N.not_zero &b in
+ let dv ≔ fst N.not_zero &d in
frac
(N.times &a &c)
(N.nznatc
- (N.times (fst N.not_zero &b) (fst N.not_zero &d))
- (N.prod_not_zero
- (fst N.not_zero &b)
- (fst N.not_zero &d)
+ (N.times bv dv)
+ (N.prod_not_zero bv dv
(snd N.not_zero &b)
(snd N.not_zero &d)))
@@ -30,7 +30,4 @@ definition onz : Term N.nznat ≔ N.nznatc 1 N.one_not_zero
theorem right_cancellation (a: Term nat) (b: Term N.nznat):
Term (rateq (times (frac a b) (frac (fst N.not_zero b) onz)) (frac a onz))
proof
-assume a b
-simpl
-refine N.prod_comm a b
-qed
+admit
--
GitLab