From 164c6861860e6b52818c031f901ffeff91fca16a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 26 Jan 2016 16:56:33 +0100 Subject: Imported Upstream version 8.5 --- test-suite/bugs/closed/4429.v | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) create mode 100644 test-suite/bugs/closed/4429.v (limited to 'test-suite/bugs/closed/4429.v') diff --git a/test-suite/bugs/closed/4429.v b/test-suite/bugs/closed/4429.v new file mode 100644 index 00000000..bf0e570a --- /dev/null +++ b/test-suite/bugs/closed/4429.v @@ -0,0 +1,31 @@ +Require Import Arith.Compare_dec. +Require Import Unicode.Utf8. + +Fixpoint my_nat_iter (n : nat) {A} (f : A → A) (x : A) : A := + match n with + | O => x + | S n' => f (my_nat_iter n' f x) + end. + +Definition gcd_IT_F (f : nat * nat → nat) (mn : nat * nat) : nat := + match mn with + | (0, 0) => 0 + | (0, S n') => S n' + | (S m', 0) => S m' + | (S m', S n') => + match le_gt_dec (S m') (S n') with + | left _ => f (S m', S n' - S m') + | right _ => f (S m' - S n', S n') + end + end. + +Axiom max_correct_l : ∀ m n : nat, m <= max m n. +Axiom max_correct_r : ∀ m n : nat, n <= max m n. + +Hint Resolve max_correct_l max_correct_r : arith. + +Theorem foo : ∀ p p' p'' : nat, p'' < S (max p (max p' p'')). +Proof. + intros. + Timeout 3 eauto with arith. +Qed. -- cgit v1.2.3