Commit cf2df893 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

simplification of vstte12_combinators's proof using a new theory int.Div2

parent 1c0a7af4
......@@ -148,7 +148,7 @@ module Combinators
lemma ks_injective:
forall n1 n2: int. n1 >= 0 -> n2 >= 0 -> ks n1 = ks n2 -> n1 = n2
use import int.EuclideanDivision
use import int.Div2
let rec reduction3 (t: term) : term =
{ exists n: int. n >= 0 /\ t = ks n }
......@@ -178,7 +178,6 @@ module Combinators
end
(*
Local Variables:
compile-command: "why3ide vstte12_combinators.mlw"
......
......@@ -3,8 +3,6 @@
Require Import ZArith.
Require Import Rbase.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
(* Why3 assumption *)
Definition unit := unit.
......@@ -147,11 +145,6 @@ Axiom ks_injective : forall (n1:Z) (n2:Z), (0%Z <= n1)%Z -> ((0%Z <= n2)%Z ->
Require Import Why3. Ltac ae := why3 "alt-ergo".
Lemma mod_0_2: (EuclideanDivision.mod1 0 2 = 0)%Z.
generalize (EuclideanDivision.Div_mod 0 2).
generalize (EuclideanDivision.Mod_bound 0 2).
rewrite Zabs_eq; ae.
Qed.
(* Why3 goal *)
Theorem WP_parameter_reduction3 : forall (t:term), (exists n:Z,
......
......@@ -3,8 +3,6 @@
Require Import ZArith.
Require Import Rbase.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
(* Why3 assumption *)
Definition unit := unit.
......@@ -145,22 +143,10 @@ Axiom ks_inversion : forall (n:Z), (0%Z <= n)%Z -> ((n = 0%Z) \/
Axiom ks_injective : forall (n1:Z) (n2:Z), (0%Z <= n1)%Z -> ((0%Z <= n2)%Z ->
(((ks n1) = (ks n2)) -> (n1 = n2))).
Axiom div2 : forall (x:Z), exists y:Z, (x = (2%Z * y)%Z) \/
(x = ((2%Z * y)%Z + 1%Z)%Z).
Require Import Why3. Ltac ae := why3 "alt-ergo".
Require Import int.EuclideanDivision.
Lemma div2: forall n: Z, (0 <= n)%Z ->
(exists n': Z, 0 <= n' /\ n = 2 * n')%Z
\/ (exists n': Z, 0 <= n' /\ n = 2 * n' + 1)%Z.
intros n hn.
generalize (Div_mod n 2).
generalize (Mod_bound n 2).
intuition.
assert (e: (Zabs 2 = 2)%Z) by (simpl; auto).
rewrite e in H2.
assert (mod1 n 2 = 0 \/ mod1 n 2 = 1)%Z by omega.
destruct H0.
left; exists (div n 2); ae.
right; exists (div n 2); ae.
Qed.
(* Why3 goal *)
Theorem WP_parameter_reduction3 : forall (t:term), (exists n:Z,
......@@ -196,8 +182,7 @@ assert (n2 = 0)%Z.
destruct (ks_inversion n h1); ae.
destruct result1; auto.
intros (_, ht2).
destruct (div2 n2 h5) as [(n',h')|(n',h')].
ae.
destruct (div2 n2).
ae.
intros (_, ht2).
generalize (ht2 n2 h5); intuition.
......
......@@ -3,8 +3,6 @@
Require Import ZArith.
Require Import Rbase.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
(* Why3 assumption *)
Definition unit := unit.
......@@ -145,22 +143,10 @@ Axiom ks_inversion : forall (n:Z), (0%Z <= n)%Z -> ((n = 0%Z) \/
Axiom ks_injective : forall (n1:Z) (n2:Z), (0%Z <= n1)%Z -> ((0%Z <= n2)%Z ->
(((ks n1) = (ks n2)) -> (n1 = n2))).
Axiom div2 : forall (x:Z), exists y:Z, (x = (2%Z * y)%Z) \/
(x = ((2%Z * y)%Z + 1%Z)%Z).
Require Import Why3. Ltac ae := why3 "alt-ergo".
Require Import int.EuclideanDivision.
Lemma div2: forall n: Z, (0 <= n)%Z ->
(exists n': Z, 0 <= n' /\ n = 2 * n')%Z
\/ (exists n': Z, 0 <= n' /\ n = 2 * n' + 1)%Z.
intros n hn.
generalize (Div_mod n 2).
generalize (Mod_bound n 2).
intuition.
assert (e: (Zabs 2 = 2)%Z) by (simpl; auto).
rewrite e in H2.
assert (mod1 n 2 = 0 \/ mod1 n 2 = 1)%Z by omega.
destruct H0.
left; exists (div n 2); ae.
right; exists (div n 2); ae.
Qed.
(* Why3 goal *)
Theorem WP_parameter_reduction3 : forall (t:term), (exists n:Z,
......@@ -192,7 +178,7 @@ destruct result; auto.
intros (_, ht1).
destruct result1; auto.
intros _ _ _ _ _ _.
destruct (div2 n1 h3) as [(n',h')|(n',h')].
destruct (div2 n1) as (n',[h'|h']).
generalize (ht1 n'). ae.
generalize (ht1 n'). ae.
destruct result1_1; auto.
......
......@@ -3,8 +3,6 @@
Require Import ZArith.
Require Import Rbase.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
(* Why3 assumption *)
Definition unit := unit.
......@@ -145,22 +143,10 @@ Axiom ks_inversion : forall (n:Z), (0%Z <= n)%Z -> ((n = 0%Z) \/
Axiom ks_injective : forall (n1:Z) (n2:Z), (0%Z <= n1)%Z -> ((0%Z <= n2)%Z ->
(((ks n1) = (ks n2)) -> (n1 = n2))).
Axiom div2 : forall (x:Z), exists y:Z, (x = (2%Z * y)%Z) \/
(x = ((2%Z * y)%Z + 1%Z)%Z).
Require Import Why3. Ltac ae := why3 "alt-ergo".
Require Import int.EuclideanDivision.
Lemma div2: forall n: Z, (0 <= n)%Z ->
(exists n': Z, 0 <= n' /\ n = 2 * n')%Z
\/ (exists n': Z, 0 <= n' /\ n = 2 * n' + 1)%Z.
intros n hn.
generalize (Div_mod n 2).
generalize (Mod_bound n 2).
intuition.
assert (e: (Zabs 2 = 2)%Z) by (simpl; auto).
rewrite e in H2.
assert (mod1 n 2 = 0 \/ mod1 n 2 = 1)%Z by omega.
destruct H0.
left; exists (div n 2); ae.
right; exists (div n 2); ae.
Qed.
(* Why3 goal *)
Theorem WP_parameter_reduction3 : forall (t:term), (exists n:Z,
......@@ -194,10 +180,8 @@ intros (n1, (h3, h4)).
destruct result; auto.
intros (_, ht1).
elimtype False.
destruct (div2 n1 h3) as [(n',h')|(n',h')].
destruct (div2 n1).
ae. ae.
destruct result1; auto.
destruct result1_1; auto.
Qed.
......@@ -3,8 +3,6 @@
Require Import ZArith.
Require Import Rbase.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
(* Why3 assumption *)
Definition unit := unit.
......@@ -145,22 +143,10 @@ Axiom ks_inversion : forall (n:Z), (0%Z <= n)%Z -> ((n = 0%Z) \/
Axiom ks_injective : forall (n1:Z) (n2:Z), (0%Z <= n1)%Z -> ((0%Z <= n2)%Z ->
(((ks n1) = (ks n2)) -> (n1 = n2))).
Axiom div2 : forall (x:Z), exists y:Z, (x = (2%Z * y)%Z) \/
(x = ((2%Z * y)%Z + 1%Z)%Z).
Require Import Why3. Ltac ae := why3 "alt-ergo".
Require Import int.EuclideanDivision.
Lemma div2: forall n: Z, (0 <= n)%Z ->
(exists n': Z, 0 <= n' /\ n = 2 * n')%Z
\/ (exists n': Z, 0 <= n' /\ n = 2 * n' + 1)%Z.
intros n hn.
generalize (Div_mod n 2).
generalize (Mod_bound n 2).
intuition.
assert (e: (Zabs 2 = 2)%Z) by (simpl; auto).
rewrite e in H2.
assert (mod1 n 2 = 0 \/ mod1 n 2 = 1)%Z by omega.
destruct H0.
left; exists (div n 2); ae.
right; exists (div n 2); ae.
Qed.
(* Why3 goal *)
Theorem WP_parameter_reduction3 : forall (t:term), (exists n:Z,
......@@ -193,8 +179,8 @@ destruct result; auto.
intros (_, ht1).
destruct result1; auto.
elimtype False.
destruct (div2 n1 h3) as [(n',h')|(n',h')].
ae. ae.
destruct (div2 n1).
ae.
Qed.
......@@ -3,8 +3,6 @@
Require Import ZArith.
Require Import Rbase.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
(* Why3 assumption *)
Definition unit := unit.
......@@ -145,22 +143,10 @@ Axiom ks_inversion : forall (n:Z), (0%Z <= n)%Z -> ((n = 0%Z) \/
Axiom ks_injective : forall (n1:Z) (n2:Z), (0%Z <= n1)%Z -> ((0%Z <= n2)%Z ->
(((ks n1) = (ks n2)) -> (n1 = n2))).
Axiom div2 : forall (x:Z), exists y:Z, (x = (2%Z * y)%Z) \/
(x = ((2%Z * y)%Z + 1%Z)%Z).
Require Import Why3. Ltac ae := why3 "alt-ergo".
Require Import int.EuclideanDivision.
Lemma div2: forall n: Z, (0 <= n)%Z ->
(exists n': Z, 0 <= n' /\ n = 2 * n')%Z
\/ (exists n': Z, 0 <= n' /\ n = 2 * n' + 1)%Z.
intros n hn.
generalize (Div_mod n 2).
generalize (Mod_bound n 2).
intuition.
assert (e: (Zabs 2 = 2)%Z) by (simpl; auto).
rewrite e in H2.
assert (mod1 n 2 = 0 \/ mod1 n 2 = 1)%Z by omega.
destruct H0.
left; exists (div n 2); ae.
right; exists (div n 2); ae.
Qed.
(* Why3 goal *)
Theorem WP_parameter_reduction3 : forall (t:term), (exists n:Z,
......@@ -200,8 +186,7 @@ destruct result; auto.
intros (_, ht1).
destruct result1; auto.
elimtype False.
destruct (div2 n1 h3) as [(n',h')|(n',h')]; ae.
destruct (div2 n1); ae.
Qed.
......@@ -3,8 +3,6 @@
Require Import ZArith.
Require Import Rbase.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
(* Why3 assumption *)
Definition unit := unit.
......@@ -145,22 +143,10 @@ Axiom ks_inversion : forall (n:Z), (0%Z <= n)%Z -> ((n = 0%Z) \/
Axiom ks_injective : forall (n1:Z) (n2:Z), (0%Z <= n1)%Z -> ((0%Z <= n2)%Z ->
(((ks n1) = (ks n2)) -> (n1 = n2))).
Axiom div2 : forall (x:Z), exists y:Z, (x = (2%Z * y)%Z) \/
(x = ((2%Z * y)%Z + 1%Z)%Z).
Require Import Why3. Ltac ae := why3 "alt-ergo".
Require Import int.EuclideanDivision.
Lemma div2: forall n: Z, (0 <= n)%Z ->
(exists n': Z, 0 <= n' /\ n = 2 * n')%Z
\/ (exists n': Z, 0 <= n' /\ n = 2 * n' + 1)%Z.
intros n hn.
generalize (Div_mod n 2).
generalize (Mod_bound n 2).
intuition.
assert (e: (Zabs 2 = 2)%Z) by (simpl; auto).
rewrite e in H2.
assert (mod1 n 2 = 0 \/ mod1 n 2 = 1)%Z by omega.
destruct H0.
left; exists (div n 2); ae.
right; exists (div n 2); ae.
Qed.
(* Why3 goal *)
Theorem WP_parameter_reduction3 : forall (t:term), (exists n:Z,
......@@ -195,7 +181,7 @@ destruct result; auto.
intros (_, ht1).
destruct result1; auto.
elimtype False.
destruct (div2 n1 h3) as [(n',h')|(n',h')]; ae.
destruct (div2 n1); ae.
destruct result1_1; auto.
Qed.
......
......@@ -3,8 +3,6 @@
Require Import ZArith.
Require Import Rbase.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
(* Why3 assumption *)
Definition unit := unit.
......@@ -139,6 +137,12 @@ Axiom ks1 : ((ks 1%Z) = (App K K)).
Axiom only_K_ks : forall (n:Z), (0%Z <= n)%Z -> (only_K (ks n)).
Axiom ks_inversion : forall (n:Z), (0%Z <= n)%Z -> ((n = 0%Z) \/
((0%Z < n)%Z /\ ((ks n) = (App (ks (n - 1%Z)%Z) K)))).
Axiom ks_injective : forall (n1:Z) (n2:Z), (0%Z <= n1)%Z -> ((0%Z <= n2)%Z ->
(((ks n1) = (ks n2)) -> (n1 = n2))).
(* Why3 goal *)
Theorem ks_value : forall (n:Z), (0%Z <= n)%Z -> ((is_value (ks n)) ->
((0%Z <= n)%Z /\ (n <= 1%Z)%Z)).
......
......@@ -77,6 +77,16 @@ theory EuclideanDivision
end
(* the particular case of Euclidean division by 2 *)
theory Div2
use import Int
lemma div2:
forall x: int. exists y: int. x = 2*y \/ x = 2*y+1
end
theory ComputerDivision
(* division and modulo operators with the same conventions as
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment