Commit f86d8cf2 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix Coq proofs broken by int.Div2 realization.

parent 4c831e45
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require Import ZOdiv.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.Div2.
Require int.ComputerDivision.
Axiom div2 : forall (x:Z), exists y:Z, (x = (2%Z * y)%Z) \/
(x = ((2%Z * y)%Z + 1%Z)%Z).
Axiom mod_div_unique : forall (x:Z) (y:Z) (q:Z) (r:Z), ((0%Z <= x)%Z /\
((0%Z < y)%Z /\ ((x = ((q * y)%Z + r)%Z) /\ ((0%Z <= r)%Z /\
(r < y)%Z)))) -> ((q = (ZOdiv x y)) /\ (r = (ZOmod x y))).
......@@ -31,13 +29,30 @@ Axiom div_succ_2 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
Axiom mod2_mul2 : forall (x:Z), ((ZOmod (2%Z * x)%Z 2%Z) = 0%Z).
Axiom mod2_mul2_aux : forall (x:Z) (y:Z),
((ZOmod (y * (2%Z * x)%Z)%Z 2%Z) = 0%Z).
Axiom mod2_mul2_aux2 : forall (x:Z) (y:Z) (z:Z) (t:Z),
((ZOmod ((y * (2%Z * x)%Z)%Z + (z * (2%Z * t)%Z)%Z)%Z 2%Z) = 0%Z).
Axiom div2_mul2 : forall (x:Z), ((ZOdiv (2%Z * x)%Z 2%Z) = x).
Axiom div2_mul2_aux : forall (x:Z) (y:Z),
((ZOdiv (y * (2%Z * x)%Z)%Z 2%Z) = (y * x)%Z).
Axiom div2_add : forall (x:Z) (y:Z), (((ZOmod x 2%Z) = 0%Z) /\
((ZOmod y 2%Z) = 0%Z)) ->
((ZOdiv (x + y)%Z 2%Z) = ((ZOdiv x 2%Z) + (ZOdiv y 2%Z))%Z).
Axiom div2_sub : forall (x:Z) (y:Z), (((ZOmod x 2%Z) = 0%Z) /\
((ZOmod y 2%Z) = 0%Z)) ->
((ZOdiv (x - y)%Z 2%Z) = ((ZOdiv x 2%Z) - (ZOdiv y 2%Z))%Z).
(* Why3 goal *)
Theorem tr_mod_2 : forall (n:Z), (0%Z <= n)%Z ->
((ZOmod (n * (n + 1%Z)%Z)%Z 2%Z) = 0%Z).
intros n Hn.
destruct (div2 n) as (x,[h1|h2]).
destruct (Div2.div2 n) as (x,[h1|h2]).
rewrite h1.
replace (2 * x * (2 * x + 1)) with
(2 * (x * (2 * x + 1))) by ring.
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Div2.
(* Why3 assumption *)
Definition unit := unit.
......@@ -12,9 +13,10 @@ Inductive term :=
| S : term
| K : term
| App : term -> term -> term .
Axiom term_WhyType : WhyType term.
Existing Instance term_WhyType.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint is_value(t:term) {struct t}: Prop :=
match t with
| (K|S) => True
......@@ -22,33 +24,30 @@ Fixpoint is_value(t:term) {struct t}: Prop :=
| (App (App S v1) v2) => (is_value v1) /\ (is_value v2)
| _ => False
end.
Unset Implicit Arguments.
(* Why3 assumption *)
Inductive context :=
| Hole : context
| Left : context -> term -> context
| Right : term -> context -> context .
Axiom context_WhyType : WhyType context.
Existing Instance context_WhyType.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint is_context(c:context) {struct c}: Prop :=
match c with
| Hole => True
| (Left c1 _) => (is_context c1)
| (Right v c1) => (is_value v) /\ (is_context c1)
end.
Unset Implicit Arguments.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint subst(c:context) (t:term) {struct c}: term :=
match c with
| Hole => t
| (Left c1 t2) => (App (subst c1 t) t2)
| (Right v1 c2) => (App v1 (subst c2 t))
end.
Unset Implicit Arguments.
(* Why3 assumption *)
Inductive infix_mnmngt : term -> term -> Prop :=
......@@ -101,13 +100,11 @@ Axiom only_K_reduces : forall (t:term), (only_K t) -> exists v:term, (relTR t
v) /\ ((is_value v) /\ (only_K v)).
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint size(t:term) {struct t}: Z :=
match t with
| (K|S) => 0%Z
| (App t1 t2) => ((1%Z + (size t1))%Z + (size t2))%Z
end.
Unset Implicit Arguments.
Axiom size_nonneg : forall (t:term), (0%Z <= (size t))%Z.
......@@ -128,9 +125,6 @@ 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".
(* Why3 goal *)
......@@ -167,7 +161,7 @@ assert (n2 = 0)%Z.
destruct (ks_inversion n h1); ae.
destruct o; auto.
intros (_, ht2).
destruct (div2 n2).
destruct (Div2.div2 n2).
ae.
intros (_, ht2).
generalize (ht2 n2 h5); intuition.
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Div2.
(* Why3 assumption *)
Definition unit := unit.
Parameter qtmark : Type.
Parameter at1: forall (a:Type), a -> qtmark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
(* Why3 assumption *)
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
(* Why3 assumption *)
Inductive term :=
| S : term
| K : term
| App : term -> term -> term .
Axiom term_WhyType : WhyType term.
Existing Instance term_WhyType.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint is_value(t:term) {struct t}: Prop :=
match t with
| (K|S) => True
......@@ -37,33 +24,30 @@ Fixpoint is_value(t:term) {struct t}: Prop :=
| (App (App S v1) v2) => (is_value v1) /\ (is_value v2)
| _ => False
end.
Unset Implicit Arguments.
(* Why3 assumption *)
Inductive context :=
| Hole : context
| Left : context -> term -> context
| Right : term -> context -> context .
Axiom context_WhyType : WhyType context.
Existing Instance context_WhyType.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint is_context(c:context) {struct c}: Prop :=
match c with
| Hole => True
| (Left c1 _) => (is_context c1)
| (Right v c1) => (is_value v) /\ (is_context c1)
end.
Unset Implicit Arguments.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint subst(c:context) (t:term) {struct c}: term :=
match c with
| Hole => t
| (Left c1 t2) => (App (subst c1 t) t2)
| (Right v1 c2) => (App v1 (subst c2 t))
end.
Unset Implicit Arguments.
(* Why3 assumption *)
Inductive infix_mnmngt : term -> term -> Prop :=
......@@ -96,12 +80,12 @@ Axiom red_star_left : forall (t1:term) (t2:term) (t:term), (relTR t1 t2) ->
Axiom red_star_right : forall (v:term) (t1:term) (t2:term), (is_value v) ->
((relTR t1 t2) -> (relTR (App v t1) (App v t2))).
Axiom reducible_or_value : forall (t:term), (exists tqt:term, (infix_mnmngt t
tqt)) \/ (is_value t).
Axiom reducible_or_value : forall (t:term), (exists t':term, (infix_mnmngt t
t')) \/ (is_value t).
(* Why3 assumption *)
Definition irreducible(t:term): Prop := forall (tqt:term), ~ (infix_mnmngt t
tqt).
Definition irreducible(t:term): Prop := forall (t':term), ~ (infix_mnmngt t
t').
Axiom irreducible_is_value : forall (t:term), (irreducible t) <->
(is_value t).
......@@ -116,13 +100,11 @@ Axiom only_K_reduces : forall (t:term), (only_K t) -> exists v:term, (relTR t
v) /\ ((is_value v) /\ (only_K v)).
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint size(t:term) {struct t}: Z :=
match t with
| (K|S) => 0%Z
| (App t1 t2) => ((1%Z + (size t1))%Z + (size t2))%Z
end.
Unset Implicit Arguments.
Axiom size_nonneg : forall (t:term), (0%Z <= (size t))%Z.
......@@ -138,14 +120,11 @@ 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)))).
((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))).
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".
(* Why3 goal *)
......@@ -178,7 +157,7 @@ destruct result; auto.
intros (_, ht1).
destruct result1; auto.
intros _ _ _ _ _ _.
destruct (div2 n1) as (n',[h'|h']).
destruct (Div2.div2 n1) as (n',[h'|h']).
generalize (ht1 n'). ae.
generalize (ht1 n'). ae.
destruct result1_1; auto.
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Div2.
(* Why3 assumption *)
Definition unit := unit.
Parameter qtmark : Type.
Parameter at1: forall (a:Type), a -> qtmark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
(* Why3 assumption *)
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
(* Why3 assumption *)
Inductive term :=
| S : term
| K : term
| App : term -> term -> term .
Axiom term_WhyType : WhyType term.
Existing Instance term_WhyType.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint is_value(t:term) {struct t}: Prop :=
match t with
| (K|S) => True
......@@ -37,33 +24,30 @@ Fixpoint is_value(t:term) {struct t}: Prop :=
| (App (App S v1) v2) => (is_value v1) /\ (is_value v2)
| _ => False
end.
Unset Implicit Arguments.
(* Why3 assumption *)
Inductive context :=
| Hole : context
| Left : context -> term -> context
| Right : term -> context -> context .
Axiom context_WhyType : WhyType context.
Existing Instance context_WhyType.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint is_context(c:context) {struct c}: Prop :=
match c with
| Hole => True
| (Left c1 _) => (is_context c1)
| (Right v c1) => (is_value v) /\ (is_context c1)
end.
Unset Implicit Arguments.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint subst(c:context) (t:term) {struct c}: term :=
match c with
| Hole => t
| (Left c1 t2) => (App (subst c1 t) t2)
| (Right v1 c2) => (App v1 (subst c2 t))
end.
Unset Implicit Arguments.
(* Why3 assumption *)
Inductive infix_mnmngt : term -> term -> Prop :=
......@@ -96,12 +80,12 @@ Axiom red_star_left : forall (t1:term) (t2:term) (t:term), (relTR t1 t2) ->
Axiom red_star_right : forall (v:term) (t1:term) (t2:term), (is_value v) ->
((relTR t1 t2) -> (relTR (App v t1) (App v t2))).
Axiom reducible_or_value : forall (t:term), (exists tqt:term, (infix_mnmngt t
tqt)) \/ (is_value t).
Axiom reducible_or_value : forall (t:term), (exists t':term, (infix_mnmngt t
t')) \/ (is_value t).
(* Why3 assumption *)
Definition irreducible(t:term): Prop := forall (tqt:term), ~ (infix_mnmngt t
tqt).
Definition irreducible(t:term): Prop := forall (t':term), ~ (infix_mnmngt t
t').
Axiom irreducible_is_value : forall (t:term), (irreducible t) <->
(is_value t).
......@@ -116,13 +100,11 @@ Axiom only_K_reduces : forall (t:term), (only_K t) -> exists v:term, (relTR t
v) /\ ((is_value v) /\ (only_K v)).
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint size(t:term) {struct t}: Z :=
match t with
| (K|S) => 0%Z
| (App t1 t2) => ((1%Z + (size t1))%Z + (size t2))%Z
end.
Unset Implicit Arguments.
Axiom size_nonneg : forall (t:term), (0%Z <= (size t))%Z.
......@@ -138,14 +120,11 @@ 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)))).
((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))).
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".
(* Why3 goal *)
......@@ -160,14 +139,12 @@ Theorem WP_parameter_reduction3 : forall (t:term), (exists n:Z,
((t1 = (ks ((2%Z * n)%Z + 1%Z)%Z)) -> (result = (App K K))))) ->
match result with
| K => True
| S => (exists n:Z, (0%Z <= n)%Z /\ (t2 = (ks n))) ->
forall (result1:term), ((is_value result1) /\ forall (n:Z),
(0%Z <= n)%Z -> (((t2 = (ks (2%Z * n)%Z)) -> (result1 = K)) /\
((t2 = (ks ((2%Z * n)%Z + 1%Z)%Z)) -> (result1 = (App K K))))) ->
((is_value (App S result1)) /\ forall (n:Z), (0%Z <= n)%Z ->
(((t = (ks (2%Z * n)%Z)) -> ((App S result1) = K)) /\
((t = (ks ((2%Z * n)%Z + 1%Z)%Z)) -> ((App S result1) = (App K
K)))))
| S => (exists n:Z, (0%Z <= n)%Z /\ (t2 = (ks n))) -> forall (o:term),
((is_value o) /\ forall (n:Z), (0%Z <= n)%Z ->
(((t2 = (ks (2%Z * n)%Z)) -> (o = K)) /\
((t2 = (ks ((2%Z * n)%Z + 1%Z)%Z)) -> (o = (App K K))))) ->
((is_value (App S o)) /\ forall (n:Z), (0%Z <= n)%Z ->
((~ (t = (ks (2%Z * n)%Z))) /\ ~ (t = (ks ((2%Z * n)%Z + 1%Z)%Z))))
| (App K v1) => True
| (App S v1) => True
| (App (App S v1) v2) => True
......@@ -180,7 +157,7 @@ intros (n1, (h3, h4)).
destruct result; auto.
intros (_, ht1).
elimtype False.
destruct (div2 n1).
destruct (Div2.div2 n1).
ae. ae.
Qed.
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Div2.
(* Why3 assumption *)
Definition unit := unit.
Parameter qtmark : Type.
Parameter at1: forall (a:Type), a -> qtmark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
(* Why3 assumption *)
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
(* Why3 assumption *)
Inductive term :=
| S : term
| K : term
| App : term -> term -> term .
Axiom term_WhyType : WhyType term.
Existing Instance term_WhyType.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint is_value(t:term) {struct t}: Prop :=
match t with
| (K|S) => True
......@@ -37,33 +24,30 @@ Fixpoint is_value(t:term) {struct t}: Prop :=
| (App (App S v1) v2) => (is_value v1) /\ (is_value v2)
| _ => False
end.
Unset Implicit Arguments.
(* Why3 assumption *)
Inductive context :=
| Hole : context
| Left : context -> term -> context
| Right : term -> context -> context .
Axiom context_WhyType : WhyType context.
Existing Instance context_WhyType.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint is_context(c:context) {struct c}: Prop :=
match c with
| Hole => True
| (Left c1 _) => (is_context c1)
| (Right v c1) => (is_value v) /\ (is_context c1)
end.
Unset Implicit Arguments.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint subst(c:context) (t:term) {struct c}: term :=
match c with
| Hole => t
| (Left c1 t2) => (App (subst c1 t) t2)
| (Right v1 c2) => (App v1 (subst c2 t))
end.
Unset Implicit Arguments.
(* Why3 assumption *)
Inductive infix_mnmngt : term -> term -> Prop :=
......@@ -96,12 +80,12 @@ Axiom red_star_left : forall (t1:term) (t2:term) (t:term), (relTR t1 t2) ->
Axiom red_star_right : forall (v:term) (t1:term) (t2:term), (is_value v) ->
((relTR t1 t2) -> (relTR (App v t1) (App v t2))).
Axiom reducible_or_value : forall (t:term), (exists tqt:term, (infix_mnmngt t
tqt)) \/ (is_value t).
Axiom reducible_or_value : forall (t:term), (exists t':term, (infix_mnmngt t
t')) \/ (is_value t).
(* Why3 assumption *)
Definition irreducible(t:term): Prop := forall (tqt:term), ~ (infix_mnmngt t
tqt).
Definition irreducible(t:term): Prop := forall (t':term), ~ (infix_mnmngt t
t').
Axiom irreducible_is_value : forall (t:term), (irreducible t) <->
(is_value t).
......@@ -116,13 +100,11 @@ Axiom only_K_reduces : forall (t:term), (only_K t) -> exists v:term, (relTR t
v) /\ ((is_value v) /\ (only_K v)).
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint size(t:term) {struct t}: Z :=
match t with
| (K|S) => 0%Z
| (App t1 t2) => ((1%Z + (size t1))%Z + (size t2))%Z
end.
Unset Implicit Arguments.
Axiom size_nonneg : forall (t:term), (0%Z <= (size t))%Z.
......@@ -138,14 +120,11 @@ 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)))).
((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))).
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".
(* Why3 goal *)
......@@ -164,11 +143,11 @@ Theorem WP_parameter_reduction3 : forall (t:term), (exists n:Z,
| (App K v1) => True
| (App S v1) => True
| (App (App S v1) v2) => (exists n:Z, (0%Z <= n)%Z /\ (t2 = (ks n))) ->
forall (result1:term), ((is_value result1) /\ forall (n:Z),
(0%Z <= n)%Z -> (((t2 = (ks (2%Z * n)%Z)) -> (result1 = K)) /\
((t2 = (ks ((2%Z * n)%Z + 1%Z)%Z)) -> (result1 = (App K K))))) ->
exists n:Z, (0%Z <= n)%Z /\ ((App (App v1 result1) (App v2
result1)) = (ks n))
forall (v3:term), ((is_value v3) /\ forall (n:Z), (0%Z <= n)%Z ->
(((t2 = (ks (2%Z * n)%Z)) -> (v3 = K)) /\
((t2 = (ks ((2%Z * n)%Z + 1%Z)%Z)) -> (v3 = (App K K))))) ->
exists n:Z, (0%Z <= n)%Z /\ ((App (App v1 v3) (App v2
v3)) = (ks n))
| _ => True
end
end.
......@@ -179,7 +158,7 @@ destruct result; auto.
intros (_, ht1).
destruct result1; auto.
elimtype False.
destruct (div2 n1).
destruct (Div2.div2 n1).
ae.
Qed.
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Div2.
(* Why3 assumption *)
Definition unit := unit.
Parameter qtmark : Type.
Parameter at1: forall (a:Type), a -> qtmark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
(* Why3 assumption *)