text:
(*
(C) Copyright 2010, COQTAIL team

Project Info: http://sourceforge.net/projects/coqtail/

This library is free software; you can redistribute it and/or modify it
under the terms of the GNU Lesser General Public License as published by
the Free Software Foundation; either version 2.1 of the License, or
(at your option) any later version.

This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public
License for more details.

You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301,
USA.
*)

Require Import Arith.
Require Import Euclid.
Require Export Nle.
Require Export Nk_ind.
Require Export Compare.
Open Scope nat_scope.

(** * Definitions *)
(** Definition of divisibility *)
Inductive Ndivide a b : Prop :=
| Ndivide_intro : forall q, b = q * a -> Ndivide a b.

(** Definition of a quotient *)
Inductive Nquotient a b : nat -> Prop :=
| Nquotient_intro : forall q, b = q * a -> Nquotient a b q.

(** Definition of modulus/remainder *)
Inductive Nmod a b : nat -> Prop :=
| Nmod_intro : forall q r, b = q * a + r -> r < a -> Nmod a b r.

(** Notation *)
Notation "( a | b )" := (Ndivide a b) (at level 0) : nat_scope.

(** Definition of coprimality *)
Definition Nrel_prime p q := forall n, (n | p) -> (n | q) -> n = 1.

(** Definition of primality *)
Definition Nprime p := 1<p /\ (forall n, 1 < n < p -> ~ (n | p)).

(* begin hide *)
Lemma Nprime_intro : forall p, 1 < p -> (forall n, 1 < n < p -> ~(n | p)) -> Nprime p.
intros.
split; auto.
Qed.
(* end hide *)

(** * Basic results on prime numbers *)
(** [0] is not prime *)
Lemma Nnot_prime_0 : ~(Nprime 0).
Proof.
unfold Nprime.
intro.
destruct H.
apply le_Sn_O in H.
exact H.
Qed.

(** [1] is not prime *)
Lemma Nnot_prime_1 : ~(Nprime 1).
Proof.
unfold Nprime.
intro.
destruct H.
apply lt_irrefl in H.
exact H.
Qed.

(** A prime number is greater than or equal to [2] *)
Lemma Nprime_ge_2 : forall (p:nat), Nprime p -> 2<=p.
Proof.
intros.
destruct p.
apply Nnot_prime_0 in H.
contradiction.
destruct p.
apply Nnot_prime_1 in H.
contradiction.
unfold Nprime in H.
destruct H.
auto with arith.
Qed.

(** A composed number is not prime *)
Lemma Ncomposed_not_prime : forall n m, 1 < n -> 1 < m -> ~(Nprime (n * m)).
Proof.
intros.
intro.
destruct H1.
apply H2 with n.
split.
auto with arith.
replace n with (n*1).
destruct n.
apply le_Sn_O in H.
contradiction.
rewrite <- mult_assoc.
apply mult_S_lt_compat_l.
rewrite mult_1_l.
trivial.
auto with arith.
exists m.
ring.
Qed.

(** * Basic properties of divisibility *)
(** Compatibility with addition *)
Lemma Ndiv_plus_compat : forall p a b, (p | a) -> (p | b) -> (p | a + b).
Proof.
intros.
destruct H.
destruct H0.
apply Ndivide_intro with (q+q0).
rewrite H. rewrite H0.
ring.
Qed.

(** Product divisiblity weakening *)
Lemma Nab_div_c : forall a b c, (a * b | c) -> (a | c).
Proof.
intros.
destruct H.
apply Ndivide_intro with (q*b).
rewrite H.
ring.
Qed.

(** A divisor is usually nonzero *)
Lemma Ndiv_non_0 : forall a b, (a | b) -> 1 <= b -> 1 <= a.
Proof.
intros.
destruct a.
destruct H.
rewrite mult_0_r in H.
rewrite H in H0.
exact H0.
auto with arith.
Qed.

(** Any number divides [0] *)
Lemma Ndiv_0 : forall a, (a | 0).
intros.
apply Ndivide_intro with 0.
ring.
Qed.

(** [1] divides any number *)
Lemma Ndiv_1 : forall a, (1 | a).
intros.
apply Ndivide_intro with a.
ring.
Qed.

(** Not divisor implies nonzero *)
Lemma Nnon_div_non_zero : forall a b, ~( a | b) -> b > 0.
intros.
destruct b.
destruct H.
apply Ndiv_0.
auto with arith.
Qed.

(** [n] divides [n] *)
Lemma Ndiv_n_n : forall n, (n|n).
Proof.
intro.
apply Ndivide_intro with 1.
ring.
Qed.

(** * Basic properties of quotient *)
(** Quotient implies divisibility *)
Lemma Nquotient_div : forall a b q, Nquotient a b q -> (a | b).
Proof.
intros.
destruct H.
apply Ndivide_intro with q.
auto.
Qed.

(** Compatibility with order *)
Lemma Nquotient_le_compat : forall a b c q p,
  Nquotient a b q -> Nquotient a c p -> 1 <= b <= c -> q <= p.
Proof.
intros.
assert (1<=a).
apply Ndiv_non_0 with b.
apply Nquotient_div with q.
exact H.
destruct H1.
exact H1.
assert (exists a',a=S a').
destruct a.
apply le_Sn_O in H2.
contradiction.
exists a.
reflexivity.
destruct H3.
destruct H.
destruct H0.
destruct H1.
rewrite H in H4.
rewrite H0 in H4.
rewrite H3 in H4.
apply mult_S_le_reg_l with x.
assert (S x*q=q*S x).
ring.
assert (S x*q0=q0*S x).
ring.
rewrite H5.
rewrite H6.
exact H4.
Qed.

(** * Properties of divisibility *)

(** Transitivity *)
Lemma Ndiv_trans : forall a b c, (a | b) -> (b | c) -> (a | c).
Proof.
intros.
destruct H.
destruct H0.
exists (q*q0).
rewrite H0.
rewrite H.
ring.
Qed.

(** Simplification of addition *)
Lemma Ndiv_plus_simpl : forall a b c, (a | b + c) -> (a | b) -> (a | c).
Proof.
intros.
destruct b.
destruct H.
apply Ndivide_intro with q.
auto with arith.

destruct H.
destruct H0.
apply Ndivide_intro with (q-q0).
assert (q0<=q).
apply Nquotient_le_compat with a (S b) (S b+c).
apply Nquotient_intro. exact H0.
apply Nquotient_intro. exact H.
split.
auto with arith.
auto with arith.
apply Nle_plus in H1.
destruct H1.
rewrite H1.
assert (q0+x-q0=x).
apply minus_plus.
rewrite H2.
rewrite H1 in H.
rewrite H0 in H.
rewrite mult_plus_distr_r in H.
rewrite plus_comm in H.
apply plus_reg_l with (q0*a).
rewrite plus_comm.
rewrite H.
auto with arith.
Qed.

(** Right implification of subtraction *)
Lemma Ndiv_minus_simpl_r : forall a b c, b >= c -> (a | b - c) -> (a | c) -> (a | b).
Proof.
intros.
apply Nle_plus in H.
destruct H.
rewrite H in * |- *.
rewrite minus_plus in H0.
apply Ndiv_plus_compat; auto.
Qed.

(** Left implification of subtraction *)
Lemma Ndiv_minus_simpl_l : forall a b c, b >= c -> (a | b - c) -> (a | b) -> (a | c).
Proof.
intros.
apply Nle_plus in H.
destruct H.
rewrite H in * |- *.
rewrite minus_plus in H0.
rewrite plus_comm in H1.
apply Ndiv_plus_simpl with x; auto.
Qed.

(** Weak compatibility with multiplication *)
Lemma Ndiv_mult_compat : forall a b q, (a | b) -> (a | b * q).
Proof.
intros.
destruct H.
apply Ndivide_intro with (q0*q).
rewrite H.
ring.
Qed.

(** Strong compatibility with multiplication *)
Lemma Ndiv_strong_mult_compat : forall a b q, (a|b) -> (a * q | b * q).
Proof.
intros.
destruct H.
apply Ndivide_intro with (q0).
rewrite H.
ring.
Qed.

(** Simplification of common factor *)
Lemma Ndiv_mult_simpl : forall a b q, q <> 0 -> (a * q | b * q) -> (a | b).
Proof.
intros.
destruct H0.
destruct q.
contradiction H.
reflexivity.
rewrite mult_assoc in H0.
assert (S q*b=S q*(q0*a)).
rewrite mult_comm.
rewrite H0.
ring.
assert (b=q0*a).
(* begin hide *)
  Lemma toto : forall a b q, S q * a = S q * b -> a = b.
  induction a.
  intros.
  rewrite mult_0_r in H.
  symmetry in H.
  apply mult_is_O in H.
  destruct H.
  discriminate H.
  auto.
  intros.
  destruct b.
  rewrite mult_0_r in H.
  discriminate H.
  assert (a=b).
  rewrite mult_succ_r in H.
  rewrite mult_succ_r in H.
  assert (S q  + S q * a= S q + S q * b).
  rewrite plus_comm.
  rewrite H.
  ring.
  apply plus_reg_l in H0.
  apply IHa with q.
  auto.
  rewrite H0.
  auto.
  Qed.
(* end hide *)
apply toto with q.
rewrite mult_comm.
rewrite H0.
ring.
apply Ndivide_intro with q0.
auto.
Qed.

(** Divisibility implies order *)
Lemma Ndiv_le : forall n p, 0 < p -> (n | p) -> n <= p.
Proof.
intros.
destruct H0.
destruct p.
apply lt_irrefl in H. contradiction.
destruct n.
auto with arith.
destruct q.
simpl in H0.
discriminate H0.
replace (S n) with (1*S n).
rewrite H0.
apply mult_le_compat.
auto with arith.
auto with arith.
rewrite mult_1_l.
trivial.
Qed.

(** Dividable by [0] implies zero *)
Lemma Ndiv_0_n : forall n, (0 | n) -> n = 0.
Proof.
destruct n.
trivial.
intro.
destruct H.
rewrite mult_0_r in H.
discriminate H.
Qed.

(** * Properties of coprimes *)

(** [n] and [n] are usually not coprime *)
Lemma Nnon_rel_prime_n_n : forall n, n <> 1 -> ~(Nrel_prime n n).
Proof.
intro.
intro.
intro.
unfold Nrel_prime in H0.
assert (n=1).
apply H0.
apply Ndiv_n_n.
apply Ndiv_n_n.
contradiction.
Qed.

(** Compatibility with modulus *)
Theorem Nrel_prime_mod : forall a b r, Nrel_prime a b -> Nmod a b r -> Nrel_prime a r.
Proof.
intros.
destruct H0.
unfold Nrel_prime in H.
unfold Nrel_prime.
intros.
assert (n|b).
rewrite H0.
apply Ndiv_plus_compat.
rewrite mult_comm.
apply Ndiv_mult_compat.
auto.
auto.
apply H.
auto.
auto.
Qed.

(** Commutativity *)
Lemma Nrel_prime_comm : forall a b, Nrel_prime a b -> Nrel_prime b a.
Proof.
intros.
intro.
intros.
apply H.
auto.
auto.
Qed.

(** Weakening from primality to coprimality *)
Lemma Nprime_le_rel_prime : forall n p, Nprime p -> 1 < n < p -> Nrel_prime n p.
Proof.
intros.
destruct H0.
destruct H.
intro.
intros.
assert (0<n0).
apply Ndiv_non_0 with n.
auto.
auto with arith.
assert (n0<p).
apply le_trans with (S n).
apply le_n_S.
apply Ndiv_le.
auto with arith.
trivial.
auto.
destruct n0.
apply Ndiv_0_n in H3.
rewrite H3 in H0.
inversion H0.
destruct n0.
trivial.
apply H2 in H4.
contradiction.
split.
auto with arith.
auto.
Qed.

(** A coprime of [0] is [1] *)
Lemma Nrel_prime_0 : forall n, Nrel_prime n 0 -> n = 1.
Proof.
intros.
apply H.
apply Ndiv_n_n.
apply Ndiv_0.
Qed.

(** Any number is coprime with [1] *)
Lemma Nrel_prime_1 : forall n, Nrel_prime n 1.
Proof.
intros.
intro.
intros.
destruct n0.
destruct H0.
rewrite mult_0_r in H0. auto.
apply Ndiv_le in H0.
destruct n0.
auto.
inversion H0.
inversion H2.
auto.
Qed.

(** * Gauss theorem *)
Theorem Ngauss : forall a b c, (a | b * c) -> Nrel_prime a b -> (a | c).
Proof.
apply (nat_strong_ind (fun a =>  forall b c, (a|b*c) -> Nrel_prime a b -> (a|c))).
intros.
destruct H.
rewrite mult_0_r in H.
apply mult_is_O in H.
destruct H.
rewrite H in H0.
apply Nnon_rel_prime_n_n in H0.
contradiction.
auto with arith.
rewrite H.
apply Ndiv_0.

intros.
destruct n.
apply Ndiv_1.

destruct H0.
assert (diveucl b (S (S n))).
apply eucl_dev.
auto with arith.
destruct H2.
assert (diveucl c (S(S n))).
apply eucl_dev.
auto with arith.
destruct H2.
rewrite e in H0.
rewrite e0 in H0.
rewrite mult_plus_distr_l in H0.
rewrite mult_plus_distr_r in H0.
rewrite mult_plus_distr_r in H0.
assert (S (S n)|r*r0).
apply Ndiv_plus_simpl with (q0 *S( S n) * r0).
apply Ndiv_plus_simpl with (r * (q1 * S(S n))).
apply Ndiv_plus_simpl with (q0 * S(S n) * (q1 * S(S n))).
apply Ndivide_intro with q.
rewrite <- H0.
ring.
apply Ndivide_intro with (q0*S(S n)*q1).
ring.
apply Ndivide_intro with (r*q1).
ring.
apply Ndivide_intro with (r0*q0).
ring.
destruct H2.
assert (Nrel_prime (S(S n)) r).
apply Nrel_prime_mod with b.
auto.
apply Nmod_intro with q0.
auto.
auto.
assert (r|q2).
apply H with (S(S n)).
auto with arith.
apply Ndivide_intro with r0.
rewrite mult_comm.
rewrite <- H2.
ring.
apply Nrel_prime_comm.
auto.
assert (S(S n)*r | r*r0).
rewrite H2.
rewrite mult_comm.
apply Ndiv_strong_mult_compat.
auto.
assert (S(S n)|r0).
apply Ndiv_mult_simpl with r.
destruct r.
rewrite plus_0_r in e.
assert (S(S n)|b).
apply Ndivide_intro with q0.
auto.
assert (S(S n)=1).
apply H1.
apply Ndiv_n_n.
auto.
discriminate H7.
auto with arith.
destruct H5.
apply Ndivide_intro with q3.
rewrite mult_comm.
rewrite H5.
ring.
rewrite e0.
apply Ndiv_plus_compat.
rewrite mult_comm.
apply Ndiv_mult_compat.
apply Ndiv_n_n.
auto.
Qed.

(** * Decidability of divisibility *)

(** Algorithm to compute a remainder modulus a number *)
Fixpoint Ndiv_mod_algo (n m:nat) {struct m} : nat :=
match n with
| 0 => 0
| S n' =>
  match m with
  | 0 => 0
  | S m' =>
    let tmp:=S (Ndiv_mod_algo n m') in
    match beq_nat n tmp with
    | true => 0
    | false => tmp
    end
  end
end.

(** Algorithm to decide divisibility *)
Definition Ndiv_algo (n m:nat) : bool :=
  beq_nat (Ndiv_mod_algo n m) 0.

(** [m] mod [n] equals [m] if [n] is greater than [m] *)
Lemma Ndiv_mod_l0 : forall n m, m < n -> Ndiv_mod_algo n m = m.
Proof.
induction m.
intros. destruct n. inversion H. compute. trivial.
intros.
destruct n.
inversion H.
simpl.
replace (Ndiv_mod_algo (S n) m) with m.
replace (beq_nat n m) with false.
reflexivity.
  (* begin hide *)
  Lemma eq_nat_correct : forall n m, n<>m -> false=beq_nat n m.
  Proof.
  intros n.
  induction n.
  destruct m.
  intros.
  contradiction H. reflexivity.
  intros.
  compute. reflexivity.
  induction m.
  compute. reflexivity.
  simpl.
  intros.
  apply IHn.
  auto with arith.
  Qed.
(* end hide *)
apply eq_nat_correct.
intro.
rewrite H0 in H.
apply lt_irrefl in H. contradiction.
symmetry.
apply IHm.
auto with arith.
Qed.

(** Simplification of addition *)
Lemma Ndiv_mod_l1 : forall n m, n > 0 -> Ndiv_mod_algo n (m + n) = Ndiv_mod_algo n m.
Proof.
intros n m. pattern m. apply nat_strong_ind.
intros. simpl.
induction n.
reflexivity.
simpl.
replace (Ndiv_mod_algo (S n) n) with n.
replace (beq_nat n n) with true.
reflexivity. apply beq_nat_refl.
symmetry.
apply Ndiv_mod_l0.
auto with arith.
intros.
induction n.
simpl. reflexivity.
simpl.
replace (Ndiv_mod_algo (S n) (n0+S n)) with (Ndiv_mod_algo (S n) n0).
Focus 2.
symmetry.
apply H.
auto with arith.
auto with arith.
auto.
Qed.

(** Correctness of divisibility algorithm *)
Theorem Ndiv_algo_correct : forall n m, n > 0 -> (n | m) -> Ndiv_algo n m=true.
Proof.
destruct n.
intros.
inversion H.
intro. pattern m.
apply nat_strong_ind.
intros.
compute. trivial.
intros.
unfold Ndiv_algo.
destruct H1.
destruct q.
simpl in H1.
inversion H1.
rewrite mult_succ_l in H1.
rewrite H1.
rewrite Ndiv_mod_l1.
apply H.
apply le_trans with (q*S n+n).
auto with arith.
rewrite plus_comm in H1.
simpl in H1.
apply eq_add_S in H1.
rewrite H1.
rewrite plus_comm.
auto with arith.
auto with arith.
exists q.
auto.
auto.
Qed.

(* The remainder is a remainder (strong condition) *)
Lemma Ndiv_mod_algo_rem : forall n m r, n > 0 -> Ndiv_mod_algo n m = r -> r < n.
Proof.
induction m.
intros.
destruct n. inversion H. compute in H0. rewrite <- H0. auto with arith.
intros.
destruct n. inversion H.
simpl in H0.
assert (Ndiv_mod_algo (S n) m<(S n)).
apply IHm. auto with arith. auto.
apply le_le_S_eq in H1.
destruct H1.
apply le_S_n in H1.
apply le_lt_n_Sm in H1.
apply lt_S_n in H1.
destruct (beq_nat n (Ndiv_mod_algo (S n) m)).
rewrite <- H0. auto with arith.
rewrite <- H0.
apply lt_n_S. auto.
apply eq_add_S in H1.
rewrite H1 in H0.
rewrite <- beq_nat_refl in H0.
rewrite <- H0.
auto with arith.
Qed.

(* The remainder is lower than or equal to number itself *)
Lemma Ndiv_mod_algo_rem2 : forall n m r, n > 0 -> Ndiv_mod_algo n m = r -> r <= m.
Proof.
induction m.
intros.
destruct n; compute in H0; rewrite <- H0; auto with arith.
intros.
simpl in H0.
destruct n. inversion H.
destruct (beq_nat (S n) (S (Ndiv_mod_algo (S n) m))).
rewrite <- H0. auto with arith.
destruct r.
inversion H0.
apply eq_add_S in H0.
apply le_n_S.
apply IHm.
auto.
auto.
Qed.

(** Completeness of modulus algorithm *)
Theorem Ndiv_mod_algo_complete : forall n m r, n > 0 -> Ndiv_mod_algo n m = r ->
(n | m - r).
Proof.
destruct n.
intros. inversion H.
intro m. pattern m. apply nat_strong_ind.
intros.
compute in H0.
rewrite <- H0.
simpl.
apply Ndiv_0.
intros.
simpl in H1.
case (lt_eq_lt_dec (S n) n0).
intros.
destruct s.
Focus 2.
rewrite <- e in H1.
replace (Ndiv_mod_algo (S n) (S n)) with (Ndiv_mod_algo (S n) (0+S n)) in H1.
rewrite Ndiv_mod_l1 in H1.
simpl in H1.
destruct n.
simpl in H1.
rewrite <- H1.
rewrite <- e.
simpl.
exists 2. ring.
simpl in H1.
rewrite <- H1.
rewrite e.
simpl.
rewrite <- minus_n_O.
apply Ndiv_n_n.
auto with arith.
simpl. auto.
Focus 2.
intro.
replace (Ndiv_mod_algo (S n) n0) with n0 in H1.
apply le_le_S_eq in l.
destruct l.
assert (n<>n0).
intro. rewrite H3 in H2. apply lt_irrefl in H2. auto.
apply eq_nat_correct in H3.
rewrite <- H3 in H1.
rewrite <- H1.
rewrite <- minus_diag_reverse.
apply Ndiv_0.
apply eq_add_S in H2.
rewrite H2 in H1.
rewrite <- beq_nat_refl in H1.
rewrite <- H1.
rewrite <- minus_n_O.
rewrite H2.
apply Ndiv_n_n.
symmetry.
apply Ndiv_mod_l0.
auto.

assert (exists d, n0=S n+d).
apply Nle_plus.
auto with arith.
destruct H2.
rewrite H2 in H1.
assert (Ndiv_mod_algo (S n) (S n+x)=Ndiv_mod_algo (S n) (x+S n)).
rewrite plus_comm. auto.
rewrite H3 in H1.
clear H3.
rewrite Ndiv_mod_l1 in H1.
rewrite H2.
replace (S (S n+x)) with (S n+S x).
Focus 2.
auto with arith.
replace (S n+S x-r) with (S n+(S x-r)).
Focus 2.
apply plus_minus.
replace (r+(S n+(S x-r))) with (S n+r+(S x-r)).
Focus 2.
rewrite plus_assoc.
auto with arith.
Focus 2.
assert (S x=r+(S x-r)).
symmetry.
apply le_plus_minus_r.
destruct (beq_nat n (Ndiv_mod_algo (S n) x)).
rewrite <- H1. auto with arith.
destruct r. inversion H1.
apply eq_add_S in H1.
apply le_n_S.
apply Ndiv_mod_algo_rem2 with (S n).
auto with arith.
auto.
rewrite H3.
rewrite plus_assoc.
rewrite minus_plus.
auto.
apply Ndiv_plus_compat.
apply Ndiv_n_n.
apply H.
rewrite plus_Snm_nSm in H2.
apply le_trans with (S x+n).
auto with arith.
rewrite plus_comm.
rewrite <- H2.
auto with arith.
auto with arith.
auto.
auto with arith.
Qed.

(** Completeness of the divisibility algorith *)
Theorem Ndiv_algo_complete : forall n m, n>0 -> Ndiv_algo n m=true -> (n | m).
Proof.
intros.
unfold Ndiv_algo in H0.
symmetry in H0.
apply beq_nat_eq in H0.
replace m with (m-0).
apply Ndiv_mod_algo_complete.
auto.
auto.
auto with arith.
Qed.

(** * Greatest strict divisor *)
(** Algorithm to compute the greatest divisor lower than a number *)
Fixpoint Ngreatest_div_le (n:nat) (p:nat) {struct n}: nat :=
match n with
| 0 | 1 => 1
| S n =>
    if Ndiv_algo (S n) p then (S n)
    else Ngreatest_div_le n p
end.

(** Algorithm to compute the greatest strict divisor of a number *)
Definition Ngreatest_div (p:nat) : nat :=
  Ngreatest_div_le (pred p) p.

(** The greatest divisor is a divisor *)
Lemma Ngreatest_div_le_div : forall p n, p>1 -> (Ngreatest_div_le n p | p).
Proof.
induction n.
intros.
compute. apply Ndiv_1.
intros.
simpl.
destruct n. apply Ndiv_1.
assert(Ndiv_algo (S(S n)) p=true -> (S(S n)|p)).
intros. apply Ndiv_algo_complete. auto with arith. auto.
destruct (Ndiv_algo (S(S n)) p).
apply H0. auto.
auto.
Qed.

(** The greatest strict divisor is a divisor *)
Theorem Ngreatest_div_div : forall p, p > 1 -> (Ngreatest_div p | p).
Proof.
intros.
apply Ngreatest_div_le_div.
auto.
Qed.

(** The greatest divisor lower than a number is a lower than that number *)
Theorem Ngreatest_div_le_le : forall n p, n > 0 -> Ngreatest_div_le n p <= n.
Proof.
intros.
induction n.
inversion H.
simpl.
destruct n.
auto.
destruct (Ndiv_algo (S (S n)) p).
auto.
eapply le_trans.
eapply IHn. auto with arith.
auto with arith.
Qed.

(** The greatest divisor is a monotonous function *)
Theorem Ngreatest_div_le_monotone : forall n n' p,
  n <= n' -> Ngreatest_div_le n p <= Ngreatest_div_le n' p.
Proof.
intros.
induction H.
auto.
eapply le_trans.
eexact IHle.
assert (Ndiv_algo (S m) p=true -> Ngreatest_div_le (S m) p=S m).
intros.
simpl.
destruct m. auto.
rewrite H0. auto.
assert (Ndiv_algo (S m) p=false -> Ngreatest_div_le (S m) p=Ngreatest_div_le m p).
intros.
simpl.
destruct m. compute. auto.
rewrite H1. auto.
destruct (Ndiv_algo (S m) p).
rewrite H0.
destruct m. compute. auto.
eapply le_trans.
eapply Ngreatest_div_le_le. auto with arith.
auto with arith. auto.
rewrite H1. auto. auto.
Qed.

(** The greatest divisor is a the greatest divisor *)
Theorem Ngreatest_div_le_greatest : forall n p q,
  p>1 -> q>=1 -> q<p -> q<=n -> (q | p) -> q <= Ngreatest_div_le n p.
Proof.
intros.
replace q with (Ngreatest_div_le q p).
apply Ngreatest_div_le_monotone. auto.
destruct q.
inversion H0.
simpl.
destruct q.
auto.
apply Ndiv_algo_correct in H3.
rewrite H3. auto. auto with arith.
Qed.

(** The greatest strict divisor is a the greatest strict divisor *)
Theorem Ngreatest_div_greatest : forall p q,
  p>1 -> q>=1 -> q<p -> (q | p) -> q <= Ngreatest_div p.
Proof.
intros.
apply Ngreatest_div_le_greatest; auto.
destruct p. inversion H.
simpl. auto with arith.
Qed.

(** The greatest strict divisor is strict *)
Theorem Ngreatest_div_lt_p : forall n, n > 1 -> Ngreatest_div n < n.
Proof.
intros.
destruct n.
inversion H.
destruct n.
inversion H. inversion H1.
unfold lt.
apply le_n_S.
unfold Ngreatest_div.
replace (pred(S(S n))) with (S n).
apply Ngreatest_div_le_le.
auto with arith.
auto with arith.
Qed.

(** The greatest strict divisor is nonzero *)
Theorem Ngreatest_div_le_1 : forall n, Ngreatest_div n>=1.
Proof.
intros.
destruct n.
compute. auto.
destruct n. compute. auto.
apply Ngreatest_div_greatest.
auto with arith.
auto.
auto with arith.
apply Ndiv_1.
Qed.

(** * Decidability of primality with greatest strict divisor *)
(** Implication of greatest strict divisor on primality *)
Theorem Ngreatest_div_1_prime : forall p, p > 1 -> Ngreatest_div p = 1 -> Nprime p.
Proof.
intro.
destruct p.
intros. inversion H.
destruct p.
intros. inversion H. inversion H2.

intros.
split.
auto.
intros.
intro.
apply Ngreatest_div_greatest in H2.
rewrite H0 in H2.
destruct H1.
assert(1<1).
eapply le_trans.
eapply H1. auto.
inversion H4. inversion H6.
auto with arith.
destruct H1.
auto with arith.
destruct H1.
auto with arith.
Qed.

(** Implication of primality greatest divisor *)
Theorem Nprime_greatest_div_le_1 : forall n p, n<p -> Nprime p -> Ngreatest_div_le n p=1.
Proof.
induction n.
intros.
compute. auto.
intros.
simpl.
destruct n.
auto.
assert(~(Ndiv_algo (S (S n)) p=true)).
intro.
destruct H0.
apply H2 with (S(S n)).
split.
auto with arith. auto.
apply Ndiv_algo_complete.
auto with arith. auto.
destruct (Ndiv_algo (S (S n)) p).
contradiction H1. auto.
apply IHn.
auto with arith.
auto.
Qed.

(** Implication of primality greatest strict divisor *)
Theorem Nprime_greatest_div_1 : forall p, Nprime p -> Ngreatest_div p=1.
Proof.
intros.
apply Nprime_greatest_div_le_1.
destruct H.
inversion H;
auto with arith. auto.
Qed.

(** * Lowest strict divisor *)
(** Algorithm to compute the lowest divisor greater than a number *)
Fixpoint Nleast_div_ge (n p:nat) {struct n} : nat :=
match n with
| 0 => p
| S n =>
    if Ndiv_algo (p-S n) p then p-S n
    else Nleast_div_ge n p
end.

(** Algorithm to compute lowest strict divisor *)
Definition Nleast_div p := Nleast_div_ge (p-2) p.

(** Lowest divisor is a divisor *)
Lemma Nleast_div_ge_div : forall p n, p>1 -> n < p -> (Nleast_div_ge n p | p).
Proof.
induction n.
intros.
compute. apply Ndiv_n_n.
intros.
simpl.
assert (Ndiv_algo (p-S n) p=true -> (p-S n|p)).
apply Ndiv_algo_complete.
unfold gt.
apply (minus_le_compat_r (S (S n)) p (S n)) in H0.
rewrite <- minus_Sn_m in H0.
rewrite <- minus_n_n in H0.
eapply le_trans.
eapply H0. auto. auto.
destruct (Ndiv_algo (p-S n) p).
apply H1. auto.
apply IHn. auto.
auto with arith.
Qed.

(** Lowest divisor is usually greater than [1] *)
Theorem Nleast_div_ge_gt_1 : forall n p, p > 1 -> S n < p -> 1 < Nleast_div_ge n p.
Proof.
induction n.
intros.
compute. auto.
intros.
simpl.
destruct (Ndiv_algo (p-S n) p).
apply (minus_le_compat_r (S(S(S n))) p (S n)) in H0.
rewrite <- minus_Sn_m in H0.
rewrite <- minus_Sn_m in H0.
rewrite <- minus_n_n in H0.
auto. auto. auto.
apply IHn.
auto. auto with arith.
Qed.

(** Lowest strict divisor is greater than [1] *)
Theorem Nleast_div_gt_1 : forall p, p > 1 -> 1 < Nleast_div p.
Proof.
intros.
apply Nleast_div_ge_gt_1.
auto.
unfold lt.
assert(p>=2).
auto with arith.
apply Nle_plus in H0.
destruct H0.
rewrite H0.
rewrite minus_plus.
auto with arith.
Qed.

(** Lowest strict divisor is a divisor *)
Theorem Nleast_div_div : forall p, p>1 -> (Nleast_div p | p).
Proof.
intros.
apply Nleast_div_ge_div.
auto.
auto with arith.
Qed.

(** Lowest divisor greater than a number is greater than that number *)
Theorem Nleast_div_ge_ge : forall n p, n < p -> Nleast_div_ge n p >= p - n.
Proof.
induction n.
intros.
simpl.
rewrite <- minus_n_O.
auto.
intros.
simpl.
destruct (Ndiv_algo (p-S n) p).
auto.
unfold ge.
apply le_trans with (p-n).
apply minus_le_compat_l.
auto.
apply IHn. auto with arith.
Qed.

(** Lowest divisor is a monotonous function *)
Theorem Nleast_div_ge_monotone : forall n n' p,
  n <= n' -> n' < p -> Nleast_div_ge n p >= Nleast_div_ge n' p.
Proof.
intros.
induction H.
auto.
simpl.
destruct (Ndiv_algo (p-S m) p).
apply le_trans with (p-m).
apply minus_le_compat_l.
auto.
apply le_trans with (p-n).
apply minus_le_compat_l.
auto.
apply Nleast_div_ge_ge.
apply le_trans with (S m).
auto with arith.
auto with arith.
apply IHle.
auto with arith.
Qed.

(** Lowest divisor is lowest divisor *)
Theorem Nleast_div_ge_least : forall n p q,
  p > 1 -> q >= 1 -> q < p -> n < p -> q >= p-n -> (q | p) -> Nleast_div_ge n p <= q.
Proof.
intros.
replace q with (Nleast_div_ge (p-q) p).
apply Nleast_div_ge_monotone.
unfold ge in H3.
destruct (le_dec n p).
apply (plus_le_compat_l (p-n) q n) in H3.
rewrite le_plus_minus_r  in H3.
apply (minus_le_compat_r p (n+q) q) in H3.
rewrite plus_comm in H3.
rewrite minus_plus in H3.
auto.
auto.
apply le_trans with p.
apply le_minus.
auto.
auto.

destruct H1.
rewrite <- minus_Sn_m.
rewrite <- minus_n_n.
simpl. rewrite <- minus_n_O.
apply Ndiv_algo_correct in H4.
rewrite H4. auto. auto. auto.

rewrite <- minus_Sn_m.
simpl.
apply Ndiv_algo_correct in H4.
assert(q<=m).
auto with arith.
apply Nle_plus in H5.
destruct H5.
rewrite H5.
rewrite minus_plus.
rewrite plus_comm.
rewrite minus_plus.
rewrite H5 in H4.
rewrite plus_comm.
rewrite H4.
auto. auto. auto with arith.
Qed.

(** Lowest strict divisor is lowest divisor *)
Theorem Nleast_div_least : forall p q,
  p > 1 -> q > 1 -> q < p -> (q | p) -> Nleast_div p <= q.
Proof.
intros.
apply Nleast_div_ge_least.
auto. auto with arith. auto. auto with arith.
apply Nle_plus in H.
destruct H.
rewrite H.
rewrite minus_plus.
rewrite plus_comm.
rewrite minus_plus.
auto.
auto.
Qed.

(** * Decidability of primality with lowest strict divisor *)
(** Implication of lowest strict divisor on primality *)
Theorem Nleast_div_p_prime : forall p, p > 1 -> Nleast_div p = p -> Nprime p.
Proof.
intros.
destruct p.
inversion H.
split.
auto.
intros.
destruct H1.
intro.
apply Nleast_div_least in H3.
rewrite H0 in H3.
assert(n<n).
apply le_trans with (S p).
auto. auto.
apply lt_irrefl in H4. auto.
auto.
auto.
auto.
Qed.

(** Implication of primality on lowest divisor *)
Theorem Nprime_least_div_ge_p : forall n p, S n < p -> Nprime p -> Nleast_div_ge n p = p.
(* fixme: cette preuve est foireuse *)
induction n.
intros.
compute. auto.
intros.
destruct H0.
apply le_le_S_eq in H.
destruct H.
simpl.
assert(~(p-S n|p)).
apply H1.
split.
apply (minus_le_compat_r (S(S(S(S n)))) p (S n)) in H.
rewrite <- minus_Sn_m in H.
rewrite <- minus_Sn_m in H.
rewrite <- minus_Sn_m in H.
rewrite <- minus_n_n in H.
auto with arith.
auto.
auto.
auto with arith.
apply lt_minus.
apply le_trans with (S(S(S n))).
auto with arith. auto.
auto with arith.
auto with arith.
assert (~Ndiv_algo (p-S n) p=true).
intro.
apply H1 with (p-S n).
split.
apply (minus_le_compat_r (S(S(S(S n)))) p (S n)) in H.
rewrite <- minus_Sn_m in H.
rewrite <- minus_Sn_m in H.
rewrite <- minus_Sn_m in H.
rewrite <- minus_n_n in H.
auto with arith.
auto.
auto.
auto.
apply lt_minus.
apply le_trans with (S(S(S(S n)))).
auto. auto. auto with arith.
apply Ndiv_algo_complete.
unfold gt.
apply (minus_le_compat_r (S(S(S(S n)))) p (S n)) in H.
rewrite <- minus_Sn_m in H.
rewrite <- minus_Sn_m in H.
rewrite <- minus_Sn_m in H.
rewrite <- minus_n_n in H.
apply le_trans with 3. auto. auto. auto. auto. auto. auto. auto with arith.

destruct (Ndiv_algo (p-S n) p).
contradiction H3. auto.
apply IHn.
apply le_trans with (S(S(S(S n)))).
auto. auto.
split. auto. auto.

destruct p. inversion H.
destruct p. inversion H.
destruct p. inversion H.
do 3 apply eq_add_S in H.
rewrite H.
unfold Nleast_div_ge.
rewrite <- minus_Sn_m.
rewrite <- minus_Sn_m.
rewrite <- minus_n_n.
assert(~(Ndiv_algo 2 (S(S(S p)))=true)).
intro.
apply H1 with 2.
split. auto. auto with arith.
apply Ndiv_algo_complete. auto. auto.
destruct (Ndiv_algo 2 (S(S(S p)))).
contradiction H2. auto.
fold Nleast_div_ge.
rewrite <- H.
apply IHn.
auto.
split. auto with arith.
rewrite H.
auto.
auto.
auto.
Qed.

(** Implication of primality on lowest strict divisor *)
Theorem Nprime_least_div_p : forall p, Nprime p -> Nleast_div p = p.
Proof.
intros.
apply Nprime_least_div_ge_p.
destruct p.
apply Nnot_prime_0 in H. contradiction.
destruct p.
apply Nnot_prime_1 in H. contradiction.
rewrite minus_Sn_m.
apply le_trans with (S (S p)).
apply lt_n_S.
auto with arith. auto. auto with arith.
auto.
Qed.

(** Lowest strict divisor is prime *)
Theorem Nleast_div_prime : forall p, p>1 -> Nprime (Nleast_div p).
Proof.
intros.
split.
apply Nleast_div_gt_1.
auto.
intros.
intro.
destruct H0.
assert((n|p)).
apply Ndiv_trans with (Nleast_div p).
auto.
apply Nleast_div_div.
auto with arith.
apply Nleast_div_least in H3.
apply lt_irrefl with (Nleast_div p).
apply le_trans with (S n).
auto with arith.
auto.
auto with arith.
auto.
apply le_trans with (Nleast_div p).
auto.
apply Ndiv_le.
destruct p. inversion H.
auto with arith.
apply Nleast_div_div.
auto with arith.
Qed.

(** Lowest strict divisor is greater than [1] *)
Theorem Nleast_div_ge_2 : forall n, n > 1 -> Nleast_div n >= 2.
Proof.
intros.
assert(Nprime (Nleast_div n)).
apply Nleast_div_prime.
auto.
assert(0<=Nleast_div n).
auto with arith.
apply le_le_S_eq in H1.
destruct H1.
apply le_le_S_eq in H1.
destruct H1.
auto.
rewrite <- H1 in H0.
apply Nnot_prime_1 in H0. contradiction.
rewrite <- H1 in H0.
apply Nnot_prime_0 in H0. contradiction.
Qed.

(** Implication of lowest strict divisor on not primality *)
Theorem Nleast_div_lt_p_not_prime : forall n, n > 2 -> (Nleast_div n) < n -> ~(Nprime n).
Proof.
intros.
intro.
assert((Nleast_div n|n)).
apply Nleast_div_div.
auto with arith.
destruct H2.
destruct q.
rewrite mult_0_l in H2.
rewrite H2 in H.
inversion H.
destruct q.
rewrite mult_1_l in H2.
rewrite <- H2 in H0.
apply lt_irrefl in H0.
auto.
apply (Ncomposed_not_prime (S(S q)) (Nleast_div n)).
auto with arith.
apply Nleast_div_gt_1.
auto with arith.
rewrite H2 in H1. auto.
Qed.

(** Every number has a prime divisor *)
Theorem Nhas_prime_divisor : forall n, n > 1 -> exists p, Nprime p /\ (p | n).
Proof.
intros.
exists (Nleast_div n).
split.
apply Nleast_div_prime.
auto.
apply Nleast_div_div.
auto with arith.
Qed.

(** * Gauss theorem (prime formulation) *)
Theorem Ngauss_prime : forall a b c, (a | b * c) -> Nprime a -> (a | c) \/ (a | b).
Proof.
intros.
destruct a.
apply Nnot_prime_0 in H0. contradiction.

assert(Ndiv_algo (S(a)) b=true -> ((S(a))|b)).
intro. apply Ndiv_algo_complete. auto.
auto with arith. auto.
assert(Ndiv_algo (S a) b=false -> Nrel_prime (S a) b).
intro.
assert(~(S a|b)).
intro.
apply Ndiv_algo_correct in H3. rewrite H3 in H2. inversion H2.
auto with arith.
intro.
intros.
destruct n.
destruct H4. rewrite mult_0_r in H4. inversion H4.
destruct n.
auto.
destruct H0.
apply H6 in H4.
contradiction.
split.
auto with arith.
apply Ndiv_le in H4.
apply le_le_S_eq in H4.
destruct H4.
auto.
rewrite H4 in H5.
apply H3 in H5.
contradiction.
auto with arith.
destruct (Ndiv_algo (S a) b).
right.
apply H1.
auto.
left.
apply Ngauss with b.
apply H.
apply H2.
auto.
Qed.

(** * Compatibility of coprimality with multiplication *)
Theorem Nrel_prime_mult_compat : forall p n m,
  Nrel_prime p n -> Nrel_prime p m -> Nrel_prime p (n * m).
Proof.
intros.
intro.
intros.
destruct n0.
destruct H1.
rewrite mult_0_r in H1.
rewrite H1 in H.
destruct H2.
rewrite mult_0_r in H2.
apply mult_is_O in H2.
destruct H2.
rewrite H2 in H.
apply H.
apply Ndiv_n_n.
apply Ndiv_n_n.
rewrite H1 in H0.
rewrite H2 in H0.
apply H0.
apply Ndiv_n_n.
apply Ndiv_n_n.
destruct n0.
auto.

assert(exists pn0, Nprime pn0 /\ (pn0|(S(S n0)))).
apply Nhas_prime_divisor.
auto with arith.
destruct H3.
destruct H3.
assert((x|n*m)).
eapply Ndiv_trans.
eapply H4.
apply H2.
apply Ngauss_prime in H5.
assert(x=1).
destruct H5.
apply H0.
eapply Ndiv_trans. eapply H4. apply H1.
apply H5.
apply H.
eapply Ndiv_trans. eapply H4. apply H1.
apply H5.
rewrite H6 in H3.
apply Nnot_prime_1 in H3.
contradiction.
auto.
Qed.

(** * Primality results *)
(** Not prime implies composed *)
Theorem Nnot_prime_composed : forall n,
  n > 2 -> ~(Nprime n) -> exists p, exists q, p > 1 /\ q > 1 /\ n = p * q.
Proof.
intros.
exists(Nleast_div n).
assert(Nleast_div n|n).
apply Nleast_div_div.
auto with arith.
destruct H1.
exists q.
split.
apply Nleast_div_gt_1. auto with arith.
split.
destruct q.
rewrite mult_0_l in H1.
rewrite H1 in H.
inversion H.
destruct q.
rewrite mult_1_l in H1.
symmetry in H1.
apply Nleast_div_p_prime in H1.
apply H0 in H1. contradiction.
auto with arith.
auto with arith.
rewrite mult_comm. auto.
Qed.

(** A number if either prime or not prime *)
Theorem Nprime_or_not_prime : forall n, (Nprime n) \/ (~(Nprime n)).
Proof.
intros.
destruct n.
right. apply Nnot_prime_0.
destruct n.
right. apply Nnot_prime_1.
destruct n.
left.
apply Nprime_intro.
auto with arith.
intros.
destruct H.
inversion H.
rewrite H1 in H0.
apply lt_irrefl in H0. contradiction.
rewrite <- H2 in H0.
assert(2<2).
apply le_trans with (S m).
auto with arith. auto with arith.
apply lt_irrefl in H3. contradiction.
assert(beq_nat (Nleast_div (S(S(S n)))) (S(S(S n)))=true -> Nprime (S(S(S n)))).
intros.
apply Nleast_div_p_prime.
auto with arith.
apply beq_nat_true.
auto.
assert(beq_nat (Nleast_div (S(S(S n)))) (S(S(S n)))=false -> ~Nprime (S(S(S n)))).
intros.
assert(Nleast_div (S(S(S n)))<>(S(S(S n)))).
apply beq_nat_false.
auto.
apply not_eq in H1.
destruct H1.
apply Nleast_div_lt_p_not_prime.
auto with arith.
auto.
assert(Nleast_div (S(S(S n)))<=S(S(S n))).
apply Ndiv_le.
auto with arith.
apply Nleast_div_div.
auto with arith.
assert(S(S(S n))<S(S(S n))).
eapply le_trans.
eapply H1.
apply H2.
apply lt_irrefl in H3.
intro. auto.

destruct (beq_nat (Nleast_div (S (S (S n)))) (S (S (S n)))).
left. auto.
right. auto.
Qed.

(** A number is either prime or composed *)
Theorem Nprime_or_composed : forall n,
  n > 2 -> (Nprime n) \/ (exists p, exists q, p > 1 /\ q > 1 /\ n=p * q).
Proof.
intros.
assert(Nprime n \/ ~Nprime n).
apply Nprime_or_not_prime.
destruct H0.
left. auto.
right.
apply Nnot_prime_composed.
auto. auto.
Qed.

(** * Relation between lowest strict divisor and greatest strict divisor *)
Theorem Ngreatest_least_div_relation : forall n, n > 2 -> (Ngreatest_div n) * (Nleast_div n)=n.
Proof.
intros.
assert(Nprime n \/ ~Nprime n).
apply Nprime_or_not_prime.
destruct H0.
replace (Ngreatest_div n) with 1.
replace (Nleast_div n) with n.
ring.
symmetry.
apply Nprime_least_div_p. auto.
symmetry.
apply Nprime_greatest_div_1. auto.

assert(Q:~Nprime n).
auto. clear H0.
assert((Ngreatest_div n)*(Nleast_div n)<=n).
assert((Ngreatest_div n)|n).
apply Ngreatest_div_div. auto with arith.
destruct H0.
assert(q|n).
exists (Ngreatest_div n).
rewrite mult_comm. auto.
apply Nleast_div_least in H1.
rewrite H0 at 3.
rewrite mult_comm.
apply mult_le_compat_r.
auto.
auto with arith.
destruct q.
rewrite mult_0_l in H0. rewrite H0 in H. inversion H.
destruct q.
rewrite mult_1_l in H0.
assert(Ngreatest_div n<n).
apply Ngreatest_div_lt_p.
auto with arith.
rewrite <- H0 in H2 at 1.
apply lt_irrefl in H2.
contradiction.
auto with arith.
assert(q<=n).
apply Ndiv_le; auto. destruct n. inversion H. auto with arith.
apply le_le_S_eq in H2.
destruct H2.
auto.
rewrite H2 in H0.
destruct n.
inversion H.
assert(1<=Ngreatest_div (S n)).
apply Ngreatest_div_le_1.
apply le_le_S_eq in H3.
destruct H3.
replace q with (q*1).
rewrite H0.
rewrite H2.
apply mult_S_lt_compat_l.
auto. ring.
symmetry in H3.
apply Ngreatest_div_1_prime in H3.
apply Q in H3. contradiction.
auto with arith.

assert((Ngreatest_div n)*(Nleast_div n)>=n).
assert((Nleast_div n)|n).
apply Nleast_div_div. auto with arith.
destruct H1.
assert(q|n).
exists (Nleast_div n).
rewrite mult_comm. auto.
apply Ngreatest_div_greatest in H2.
unfold ge.
rewrite H1 at 1.
apply mult_le_compat_r.
auto.
auto with arith.
destruct q.
rewrite mult_0_l in H1.
rewrite H1 in H. inversion H.
auto with arith.
apply Ndiv_le in H2.
apply le_le_S_eq in H2.
destruct H2.
auto.
rewrite H2 in H1.
assert(Nleast_div n>=2).
apply Nleast_div_ge_2.
destruct n. inversion H.
auto with arith.
replace q with (q*1).
rewrite H1.
rewrite H2.
destruct n.
inversion H.
apply mult_S_lt_compat_l.
auto. ring.
destruct n.
inversion H.
auto with arith.

apply le_antisym; auto.
Qed.

author: coqtail

repo: coqtail

save_path: github-repos/coq/coqtail-coqtail


text:
Require Export RelDefinitions.

(** * The [RDestruct] class *)

(** ** Tactics *)

(** The [rdestruct] tactic locates and uses an [RDestruct] instance
  for a given hypothesis. *)

Ltac rdestruct H :=
  lazymatch type of H with
    | ?R ?m ?n =>
      not_evar R;
      pattern m, n;
      apply (rdestruct (R:=R) m n H);
      clear H;
      Delay.split_conjunction
  end.

(** The [rinversion] tactic is similar, but it remembers the terms
  related by the destructed hypothesis. *)

Ltac rinversion_tac H Hm Hn :=
  lazymatch type of H with
    | ?R ?m ?n =>
      not_evar R;
      pattern m, n;
      lazymatch goal with
        | |- ?Q _ _ =>
          generalize (eq_refl m), (eq_refl n);
          change ((fun x y => Delay.delayed_goal (x = m -> y = n -> Q x y)) m n);
          apply (rdestruct (R:=R) m n H);
          Delay.split_conjunction;
          intros Hm Hn
      end
  end.

Tactic Notation "rinversion" constr(H) "as" ident(Hl) "," ident(Hr) :=
  rinversion_tac H Hl Hr.

Tactic Notation "rinversion" hyp(H) :=
  let Hl := fresh H "l" in
  let Hr := fresh H "r" in
  rinversion_tac H Hl Hr.

Tactic Notation "rinversion" constr(H) :=
  let Hl := fresh "Hl" in
  let Hr := fresh "Hr" in
  rinversion_tac H Hl Hr.

(** ** Introducing the hypothesis to be destructed *)

(** The goal of [rdestruct] is usually to make progress on a goal
  relating two [match] constructions, by breaking down the terms being
  matched. The instances below will attempt to prove automatically
  that these terms are related, then destruct the resulting hypothesis
  in order to break them down and reduce the [match]es.

  If proving the destructed hypothesis automatically is not possible,
  the user can use the following tactic to introduce it manually. *)

Ltac rdestruct_assert :=
  lazymatch goal with
    | |- _ (match ?m with _ => _ end) (match ?n with _ => _ end) =>
      let Tm := type of m in
      let Tn := type of n in
      let R := fresh "R" in
      evar (R: rel Tm Tn);
      assert (R m n); subst R
  end.

(** ** [RDestruct] steps *)

(** Sometimes we want to remember what the destructed terms were.
  To make this possible, we use the following relation to wrap the
  subgoals generated by the [RDestruct] instance. *)

Definition rdestruct_result {A B} m n (Q: rel A B): rel A B :=
  fun x y => m = x /\ n = y -> Q x y.

(** To use [RDestruct] instances to reduce a goal involving pattern
  matching [G] := [_ (match m with _ end) (match n with _ end)], we
  need to establish that [m] and [n] are related by some relation [R],
  then locate an instance of [RDestruct] that corresponds to [R]. It
  is essential that this happens in one step. At some point, I tried
  to split the process in two different [RStep]s, so that the user
  could control the resolution of the [?R m n] subgoal. However, in
  situation where [RDestruct] is not the right strategy, this may
  push a [delayed rauto] into a dead end. Thankfully, now we can use
  the [RAuto] typeclass to solve the [?R m n] subgoal in one swoop. *)

Lemma rdestruct_rstep {A B} m n (R: rel A B) P (Q: rel _ _):
  RAuto (R m n) ->
  RDestruct R P ->
  P (rdestruct_result m n Q) ->
  Q m n.
Proof.
  intros Hmn HR H.
  firstorder.
Qed.

Ltac use_rdestruct_rstep m n :=
  let H := fresh in
  intro H;
  pattern m, n;
  eapply (rdestruct_rstep m n);
  [ .. | eexact H].

Global Hint Extern 40 (RStep _ (_ (match ?m with _=>_ end) (match ?n with _=>_ end))) =>
  use_rdestruct_rstep m n : typeclass_instances.

(** ** Choosing to discard or keep equations *)

(** The [RStep] above will leave us with a bunch of [rdestruct_result]
  subgoals. The next [RStep] will unpack them, and either discard or
  keep equations.

  By default, we discard equations. This is to prevent them from
  cluttering the context, possibly interfering with further steps, and
  introducing unwanted dependencies. However, the user can use the
  [rdestruct_remember] and [rdestruct_forget] tactics below to control
  this behavior. *)

CoInductive rdestruct_remember := rdestruct_remember_intro.

Ltac rdestruct_remember :=
  lazymatch goal with
    | _ : rdestruct_remember |- _ =>
      idtac
    | _ =>
      let H := fresh "Hrdestruct" in
      pose proof rdestruct_remember_intro as H
  end.

Ltac rdestruct_forget :=
  lazymatch goal with
    | H : rdestruct_remember |- _ =>
      clear H
    | _ =>
      idtac
  end.

(** The following [RStep] instance will keep or discard the equations
  in [rdestruct_result] based on the user's choice. *)

Lemma rdestruct_forget_rintro {A B} m n (Q: rel A B) x y:
  RIntro (Q x y) (rdestruct_result m n Q) x y.
Proof.
  firstorder.
Qed.

Lemma rdestruct_remember_rintro {A B} m n (Q: rel A B) x y:
  RIntro (m = x -> n = y -> Q x y) (rdestruct_result m n Q) x y.
Proof.
  firstorder.
Qed.

Ltac rdestruct_result_rintro :=
  lazymatch goal with
    | _ : rdestruct_remember |- _ =>
      eapply rdestruct_remember_rintro
    | _ =>
      eapply rdestruct_forget_rintro
  end.

Global Hint Extern 100 (RIntro _ (rdestruct_result _ _ _) _ _) =>
  rdestruct_result_rintro : typeclass_instances.

(** ** Default instance *)

(** We provide a default instance of [RDestruct] by reifying the
  behavior of the [destruct] tactic on the relational hypothesis that
  we're trying to destruct. *)

Ltac default_rdestruct :=
  let m := fresh "m" in
  let n := fresh "n" in
  let Hmn := fresh "H" m n in
  let P := fresh "P" in
  let H := fresh in
  intros m n Hmn P H;
  revert m n Hmn;
  delayed_conjunction (intros m n Hmn; destruct Hmn; delay);
  pattern P;
  eexact H.

Global Hint Extern 100 (RDestruct _ _) =>
  default_rdestruct : typeclass_instances.

(** In the special case where the terms matched on the left- and
  right-hand sides are identical, we want to destruct that term
  instead. We accomplish this by introducing a special instance of
  [RDestruct] for the relation [eq]. *)

Ltac eq_rdestruct :=
  let m := fresh "m" in
  let n := fresh "n" in
  let Hmn := fresh "H" m n in
  let P := fresh "P" in
  let H := fresh in
  intros m n Hmn P H;
  revert m n Hmn;
  delayed_conjunction (intros m n Hmn; destruct Hmn; destruct m; delay);
  pattern P;
  eexact H.

Global Hint Extern 99 (RDestruct eq _) =>
  eq_rdestruct : typeclass_instances.

author: CertiKOS

repo: coqrel

save_path: github-repos/coq/CertiKOS-coqrel


text:
(* -*- mode: coq; coq-prog-args: ("-nois" "-R" "../theories" "Coq") -*- *)
(* File reduced by coq-bug-finder from 4897 lines to 2605 lines, then from 2297 lines to 236 lines, then from 239 lines to 137 lines, then from 118 lines to 67 lines, then from 520 lines to 76 lines. *)
(** Note: The bug here is the same as the #113, that is, HoTT_coq_113.v *)
Require Import Coq.Init.Logic.
Global Set Universe Polymorphism.
Global Set Asymmetric Patterns.
Set Implicit Arguments.

Inductive sigT (A:Type) (P:A -> Type) : Type :=
  existT : forall x:A, P x -> sigT P.

Notation "{ x : A  & P }" := (sigT (fun x:A => P)) : type_scope.

Generalizable All Variables.
Definition admit {T} : T.
Admitted.
Inductive paths {A : Type} (a : A) : A -> Type :=
  idpath : paths a a.

Notation "x = y :> A" := (@paths A x y) : type_scope.
Notation "x = y" := (x = y :>_) : type_scope.
Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
  match p with idpath => u end.
Class Contr_internal (A : Type) :=
  BuildContr {
      center : A ;
      contr : (forall y : A, center = y)
    }.

Arguments center A {_}.

Inductive trunc_index : Type :=
| minus_two : trunc_index
| trunc_S : trunc_index -> trunc_index.

Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
  match n with
    | minus_two => Contr_internal A
    | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y)
  end.

Class IsTrunc (n : trunc_index) (A : Type) : Type :=
  Trunc_is_trunc : IsTrunc_internal n A.

Notation Contr := (IsTrunc minus_two).

Hint Extern 0 => progress change Contr_internal with Contr in * : typeclass_instances.

Definition path_contr `{Contr A} (x y : A) : x = y
  := admit.

Definition path_sigma' {A : Type} (P : A -> Type) {x x' : A} {y : P x} {y' : P x'}
           (p : x = x') (q : transport _ p y = y')
: existT _ x y = existT _ x' y'
  := admit.
Instance trunc_sigma `{P : A -> Type}
         `{IsTrunc n A} `{forall a, IsTrunc n (P a)}
: IsTrunc n (sigT P) | 100.

Proof.
  generalize dependent A.
  induction n; [ | apply admit ]; simpl; intros A P ac Pc.
  (exists (existT _ (center A) (center (P (center A))))).
  intros [a ?].
  refine (path_sigma' P (contr a) (path_contr _ _)).
Defined.
Inductive Bool : Set := true | false.
Definition trunc_sum' n A B `{IsTrunc n Bool, IsTrunc n A, IsTrunc n B}
: (IsTrunc n { b : Bool & if b then A else B }).
Proof.
  Set Printing All.
  Set Printing Universes.
  refine (@trunc_sigma Bool (fun b => if b then A else B) n _ _).
  (* Toplevel input, characters 23-76:
Error:
In environment
n : trunc_index
A : Type (* Top.193 *)
B : Type (* Top.194 *)
H : IsTrunc (* Set *) n Bool
H0 : IsTrunc (* Top.193 *) n A
H1 : IsTrunc (* Top.194 *) n B
The term
 "@trunc_sigma (* Top.198 Top.199 Top.200 Top.201 *) Bool
    (fun b : Bool =>
     match b return Type (* Top.199 *) with
     | true => A
     | false => B
     end) n ?49 ?50" has type
 "IsTrunc (* Top.200 *) n
    (@sig (* Top.199 Top.199 *) Bool
       (fun b : Bool =>
        match b return Type (* Top.199 *) with
        | true => A
        | false => B
        end))" while it is expected to have type
 "IsTrunc (* Top.195 *) n
    (@sig (* Set Top.197 *) Bool
       (fun b : Bool =>
        match b return Type (* Top.197 *) with
        | true => A
        | false => B
        end))" (Universe inconsistency: Cannot enforce Top.197 = Set)).
 *)
  apply admit.
Defined.

author: princeton-vl

repo: CoqGym

save_path: github-repos/coq/princeton-vl-CoqGym


text:
(** Generated by coq-of-ocaml *)
Require Import OCaml.OCaml.

Local Set Primitive Projections.
Local Open Scope string_scope.
Local Open Scope Z_scope.
Local Open Scope type_scope.
Import ListNotations.

Unset Positivity Checking.
Unset Guard Checking.

Inductive nat : Set :=
| O : nat
| S : nat -> nat.

Inductive natural : Set :=
| Zero : natural
| Succ : natural -> natural.

Fixpoint plus (plus_arg0 : natural) (plus_arg1 : natural) {struct plus_arg0}
  : natural :=
  match plus_arg0 with
  | Zero => plus_arg1
  | Succ n => Succ (plus n plus_arg1)
  end.

Fixpoint mult (mult_arg0 : natural) (mult_arg1 : natural) {struct mult_arg0}
  : natural :=
  match mult_arg0 with
  | Zero => Zero
  | Succ n => plus (mult n mult_arg1) mult_arg1
  end.

Definition synth (lf1 : natural) : natural := plus lf1 Zero.

author: yalhessi

repo: lemmaranker

save_path: github-repos/coq/yalhessi-lemmaranker


text:
(*
  Copyright (c) 2018, Inria, CEA, Northern Arizona University.
  All rights reserved.

  Redistribution and use in source and binary forms, with or without
  modification, are permitted provided that the following conditions
  are met:
  1. Redistributions of source code must retain the above copyright
     notice, this list of conditions and the following disclaimer.
  2. Redistributions in binary form must reproduce the above copyright
     notice, this list of conditions and the following disclaimer in the
     documentation and/or other materials provided with the distribution.
  3. Neither the name of the Institute nor the names of its contributors
     may be used to endorse or promote products derived from this software
     without specific prior written permission.

  THIS SOFTWARE IS PROVIDED BY THE INSTITUTE AND CONTRIBUTORS ``AS IS'' AND
  ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
  IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
  ARE DISCLAIMED.  IN NO EVENT SHALL THE INSTITUTE OR CONTRIBUTORS BE LIABLE
  FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
  DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
  OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
  HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
  OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
  SUCH DAMAGE.

  This file is part of the verification of the Contiki operating system.

  Authors: - Allan Blanchard <mail@allan-blanchard.fr>
           - Nikolai Kosmatov <nikolai.kosmatov@cea.fr>
           - Frédéric Loulergue <frederic.loulergue@nau.edu>
*)

(* ---------------------------------------------------------- *)
(* --- Lemma 'linked_ll_end'                                 --- *)
(* ---------------------------------------------------------- *)
Require Import ZArith.
Require Import Reals.
Require Import BuiltIn.
Require Import int.Int.
Require Import int.Abs.
Require Import int.ComputerDivision.
Require Import real.Real.
Require Import real.RealInfix.
Require Import real.FromInt.
Require Import map.Map.
Require Import Qedlib.
Require Import Qed.

(* --- Global Definitions (continued #2) --- *)
Require Import Memory.
Require Import Vlist.

Require Import Axiomatic.
Require Import Compound.
Require Import Axiomatic1.

Hypothesis Q_separated_linked_ll_append: forall (t : array Z),
  forall (t_1 : farray addr addr), forall (l : (list addr)),
  forall (a_1 a : addr), let a_2 := t_1.[ (shiftfield_F1_list_next a) ] in
  ((valid_rw t a 2%Z)) -> ((P_ptr_separated_from_list a_2 l)) ->
  ((P_linked_ll t t_1 a_1 a l)) -> ((separated a 2%Z a_2 2%Z)) ->
  ((P_linked_ll t t_1 a_1 a_2 ((concat l (cons a nil))))).

Hypothesis Q_inversion_linked_ll: forall (t : array Z),
  forall (t_1 : farray addr addr), forall (l : (list addr)),
  forall (a_1 a : addr), ((P_linked_ll t t_1 a_1 a l)) ->
  (((a_1 = a) /\ ((nil) = l)) \/
   (exists l_1 : (list addr), (a_1 <> a) /\
    (((cons a_1 (concat l_1 nil))) = l) /\
    ((P_ptr_separated_from_list a_1 l_1)) /\ ((valid_rw t a_1 2%Z)) /\
    ((separated a_1 2%Z a 2%Z)) /\
    ((P_linked_ll t t_1 (t_1.[ (shiftfield_F1_list_next a_1) ]) a l_1)))).

Hypothesis Q_dptr_separated_concat: forall (l_1 l : (list addr)),
  forall (a : addr),
  (((P_dptr_separated_from_list a l)) /\
   ((P_dptr_separated_from_list a l_1))) <->
  ((P_dptr_separated_from_list a ((concat l_1 (concat l nil))))).

Hypothesis Q_dptr_separated_from_cons: forall (l : (list addr)),
  forall (a_1 a : addr),
  (((P_dptr_separated_from_list a_1 l)) /\ ((separated a 2%Z a_1 1%Z))) <->
  ((P_dptr_separated_from_list a_1 ((cons a (concat l nil))))).

Hypothesis Q_dptr_separated_from_nil: forall (a : addr),
  (P_dptr_separated_from_list a (nil)).

Hypothesis Q_ptr_separated_concat: forall (l_1 l : (list addr)),
  forall (a : addr),
  (((P_ptr_separated_from_list a l)) /\ ((P_ptr_separated_from_list a l_1))) <->
  ((P_ptr_separated_from_list a ((concat l_1 (concat l nil))))).

Hypothesis Q_ptr_separated_from_cons: forall (l : (list addr)),
  forall (a_1 a : addr),
  (((P_ptr_separated_from_list a_1 l)) /\ ((separated a 2%Z a_1 2%Z))) <->
  ((P_ptr_separated_from_list a_1 ((cons a (concat l nil))))).

Hypothesis Q_ptr_separated_from_nil: forall (a : addr),
  (P_ptr_separated_from_list a (nil)).

Hypothesis Q_in_list_in_sublist: forall (l_1 l : (list addr)),
  forall (a : addr), (((P_in_list a l)) \/ ((P_in_list a l_1))) <->
  ((P_in_list a ((concat l_1 (concat l nil))))).

Goal
  forall (t : array Z),
  forall (t_1 : farray addr addr),
  forall (l : (list addr)),
  forall (a_1 a : addr),
  ((nil) <> l) ->
  ((P_linked_ll t t_1 a_1 a l)) ->
  ((t_1.[ (shiftfield_F1_list_next ((nth l (((length l))%Z - 1%Z)%Z))) ]) =
   a).

Proof.
  intros Mi Ma ll bl el Hnil NoDup.
  generalize dependent Hnil.
  induction NoDup.
  + congruence.
  + destruct l.
    - replace Datatypes.nil with nil in * by reflexivity.
      intros.
      repeat(rewrite rw_nil_concat_right).
      inversion NoDup ; subst.
      rewrite Vlist.length_cons.
      rewrite Vlist.length_nil.
      unfold nth ; simpl ; auto.
    - repeat(rewrite rw_nil_concat_right).
      rewrite Vlist.length_cons.
      replace (1 + length (a0 :: l)%list - 1) with (length (a0 :: l)%list) by omega.
      replace (nth (cons a_1 (a0 :: l)%list) (length (a0 :: l)%list))
         with (nth (a0 :: l)%list (length (a0 :: l)%list - 1)).
      * intros.
        apply IHNoDup ; auto.
        inversion NoDup ; subst.
        intros HF ; inversion HF.
      * symmetry ; apply Vlist.nth_cons.
        replace (a0 :: l)%list with (cons a0 l) by reflexivity.
        rewrite Vlist.length_cons.
        assert(0 <= length l) by (apply Vlist.length_pos) ; omega.
Qed.

author: mriiad

repo: queue

save_path: github-repos/coq/mriiad-queue


text:
(* Default settings (from HsToCoq.Coq.Preamble) *)

Generalizable All Variables.

Unset Implicit Arguments.
Set Maximal Implicit Insertion.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Require Coq.Program.Tactics.
Require Coq.Program.Wf.

(* Converted imports: *)

Require Coq.Init.Datatypes.
Require Coq.Program.Basics.
Require Data.Foldable.
Require Data.Maybe.
Require Data.OldList.
Require Data.SemigroupInternal.
Require Data.Traversable.
Require GHC.Base.
Require GHC.DeferredFix.
Require GHC.Num.
Require MonadUtils.
Require SrcLoc.
Require UniqSet.
Require Unique.
Import GHC.Base.Notations.
Import GHC.Num.Notations.

(* Converted type declarations: *)

Inductive BooleanFormula a : Type
  := Var : a -> BooleanFormula a
  |  And
   : list ((fun a_ => (SrcLoc.Located (BooleanFormula a_))%type) a) ->
     BooleanFormula a
  |  Or
   : list ((fun a_ => (SrcLoc.Located (BooleanFormula a_))%type) a) ->
     BooleanFormula a
  |  Parens
   : ((fun a_ => (SrcLoc.Located (BooleanFormula a_))%type) a) ->
     BooleanFormula a.

Definition LBooleanFormula :=
  fun a_ => (SrcLoc.Located (BooleanFormula a_))%type.

Inductive Clause a : Type
  := Mk_Clause (clauseAtoms : UniqSet.UniqSet a) (clauseExprs
    : list (BooleanFormula a))
   : Clause a.

Arguments Var {_} _.

Arguments And {_} _.

Arguments Or {_} _.

Arguments Parens {_} _.

Arguments Mk_Clause {_} _ _.

Definition clauseAtoms {a} (arg_0__ : Clause a) :=
  let 'Mk_Clause clauseAtoms _ := arg_0__ in
  clauseAtoms.

Definition clauseExprs {a} (arg_0__ : Clause a) :=
  let 'Mk_Clause _ clauseExprs := arg_0__ in
  clauseExprs.

(* Midamble *)

Import GHC.Err.
Instance Default_BooleanFormula {a} : Err.Default (BooleanFormula a) :=
  Err.Build_Default _ (And nil).

Local Fixpoint size {a} (bf: BooleanFormula a) : nat :=
  match bf with
    | Var a => 0
    | And xs => Coq.Lists.List.fold_right Nat.add 0 (Coq.Lists.List.map
        (fun lbf => match lbf with SrcLoc.L _ f => S (size f) end) xs)
    | Or xs => Coq.Lists.List.fold_right Nat.add 0 (Coq.Lists.List.map
        (fun lbf => match lbf with SrcLoc.L _ f => S (size f) end) xs)
    | Parens (SrcLoc.L _ bf) => S (size bf)
  end.

Fixpoint BooleanFormula_eq {a} `{GHC.Base.Eq_ a} (bf1 : BooleanFormula a) (bf2 : BooleanFormula a) : bool :=
  let eq' : GHC.Base.Eq_ (BooleanFormula a) := GHC.Base.eq_default BooleanFormula_eq in
    match bf1 , bf2 with
      | Var a1 , Var b1 => GHC.Base.op_zeze__ a1 b1
      | And a1 , And b1 => GHC.Base.op_zeze__ a1 b1
      | Or a1 , Or b1 => GHC.Base.op_zeze__ a1 b1
      | Parens a1 , Parens b1 => GHC.Base.op_zeze__  a1 b1
      | _ , _ => false
    end.

Instance Eq_BooleanFormula {a} `{GHC.Base.Eq_ a} : GHC.Base.Eq_ (BooleanFormula a) :=
  GHC.Base.eq_default BooleanFormula_eq.

(* We can fmap below once we cont'ified the Functor type class *)
Local Definition BooleanFormula_fmap
   : forall {a} {b}, (a -> b) -> BooleanFormula a -> BooleanFormula b :=
  fun {a} {b} => fix BooleanFormula_fmap arg_114__ arg_115__ :=
      match arg_114__ , arg_115__ with
        | f , Var a1 => Var (f a1)
        | f , And a1 => And (GHC.Base.fmap (GHC.Base.fmap (BooleanFormula_fmap f)) a1)
        | f , Or a1 => Or (GHC.Base.fmap (GHC.Base.fmap (BooleanFormula_fmap f)) a1)
        | f , Parens a1 => Parens (GHC.Base.fmap (BooleanFormula_fmap f) a1)
      end.

Local Definition BooleanFormula_traverse
    : forall {f} {a} {b},   forall `{GHC.Base.Applicative f}, (a -> f b) -> BooleanFormula a -> f (BooleanFormula b) :=
  fun {f0} {a} {b} `{GHC.Base.Applicative f0} => fix BooleanFormula_traverse arg_144__ arg_145__ :=
      match arg_144__ , arg_145__ with
        | f , Var a1 => GHC.Base.fmap  Var (f a1)
        | f , And a1 => GHC.Base.fmap And (Data.Traversable.traverse (Data.Traversable.traverse
                                                                           (BooleanFormula_traverse f)) a1)
        | f , Or a1 => GHC.Base.fmap Or
                        (@Data.Traversable.traverse _ _ _ _ f0 _ _ _ _ (Data.Traversable.traverse
                                                                          (BooleanFormula_traverse f)) a1)
        | f , Parens a1 => GHC.Base.fmap Parens
                             (@Data.Traversable.traverse _ _ _ _ f0 _ _ _ _  (BooleanFormula_traverse f) a1)
      end.

Local Definition BooleanFormula_foldMap
    : forall {m} {a},
        forall `{GHC.Base.Monoid m}, (a -> m) -> BooleanFormula a -> m :=
  fun {m} {a} `{GHC.Base.Monoid m} => fix foldMap arg_137__ arg_138__ :=
      match arg_137__ , arg_138__ with
        | f , Var a1 => f a1
        | f , And a1 => Data.Foldable.foldMap (Data.Foldable.foldMap
                                                 (foldMap f)) a1
        | f , Or a1 => Data.Foldable.foldMap (Data.Foldable.foldMap
                                                (foldMap f)) a1
        | f , Parens a1 => Data.Foldable.foldMap (foldMap f) a1
      end.

Local Definition BooleanFormula_foldr
    : forall {a} {b}, (a -> b -> b) -> b -> BooleanFormula a -> b :=
  fun {a} {b} => fix foldr arg_97__ arg_98__ arg_99__ :=
      match arg_97__ , arg_98__ , arg_99__ with
        | f , z , Var a1 => f a1 z
        | f , z , And a1 => (fun arg_101__ arg_102__ =>
                                 match arg_101__ , arg_102__ with
                                   | b5 , b6 => Data.Foldable.foldr (fun arg_103__ arg_104__ =>
                                                                      match arg_103__ , arg_104__ with
                                                                        | b3 , b4 => Data.Foldable.foldr (fun arg_105__
                                                                                arg_106__ =>
                                                                                match arg_105__
                                                                                , arg_106__ with
                                                                                | b1 ,
                                                                                b2 =>
                                                                                foldr
                                                                                f b2 b1
                                                                                end) b4 b3
                                                                      end) b6 b5
                                 end) a1 z
        | f , z , Or a1 => (fun arg_114__ arg_115__ =>
                                match arg_114__ , arg_115__ with
                                  | b5 , b6 => Data.Foldable.foldr (fun arg_116__ arg_117__ =>
                                                                     match arg_116__ , arg_117__ with
                                                                       | b3 , b4 => Data.Foldable.foldr (fun arg_118__
                                                                                arg_119__ =>
                                                                                match arg_118__
                                                                                , arg_119__ with
                                                                                | b1 , b2 =>
                                                                                foldr
                                                                                f b2 b1
                                                                                end) b4 b3
                                                                     end) b6 b5
                                end) a1 z
        | f , z , Parens a1 => (fun arg_127__ arg_128__ =>
                                    match arg_127__ , arg_128__ with
                                      | b3 , b4 => Data.Foldable.foldr (fun arg_129__ arg_130__ =>
                                                                         match arg_129__ , arg_130__ with
                                                                           | b1 , b2 => foldr f b2 b1
                                                                         end) b4 b3
                                    end) a1 z
      end.

(* Converted value declarations: *)

Definition mkVar {a} : a -> BooleanFormula a :=
  Var.

Definition mkTrue {a} : BooleanFormula a :=
  And nil.

Definition mkOr {a} `{GHC.Base.Eq_ a}
   : list (LBooleanFormula a) -> BooleanFormula a :=
  let mkOr' :=
    fun arg_0__ =>
      match arg_0__ with
      | cons x nil => SrcLoc.unLoc x
      | xs => Or xs
      end in
  let fromOr :=
    fun arg_4__ =>
      match arg_4__ with
      | SrcLoc.L _ (Or xs) => Some xs
      | SrcLoc.L _ (And nil) => None
      | x => Some (cons x nil)
      end in
  Data.Maybe.maybe mkTrue (mkOr' GHC.Base.∘ Data.OldList.nub) GHC.Base.∘
  MonadUtils.concatMapM fromOr.

Definition mkFalse {a} : BooleanFormula a :=
  Or nil.

Definition mkBool {a} : bool -> BooleanFormula a :=
  fun arg_0__ => match arg_0__ with | false => mkFalse | true => mkTrue end.

Definition mkAnd {a} `{GHC.Base.Eq_ a}
   : list (LBooleanFormula a) -> BooleanFormula a :=
  let mkAnd' :=
    fun arg_0__ =>
      match arg_0__ with
      | cons x nil => SrcLoc.unLoc x
      | xs => And xs
      end in
  let fromAnd {a} : LBooleanFormula a -> option (list (LBooleanFormula a)) :=
    fun arg_4__ =>
      match arg_4__ with
      | SrcLoc.L _ (And xs) => Some xs
      | SrcLoc.L _ (Or nil) => None
      | x => Some (cons x nil)
      end in
  Data.Maybe.maybe mkFalse (mkAnd' GHC.Base.∘ Data.OldList.nub) GHC.Base.∘
  MonadUtils.concatMapM fromAnd.

Definition simplify {a} `{GHC.Base.Eq_ a}
   : (a -> option bool) -> BooleanFormula a -> BooleanFormula a :=
  fix simplify arg_0__ arg_1__
        := match arg_0__, arg_1__ with
           | f, Var a => match f a with | None => Var a | Some b => mkBool b end
           | f, And xs =>
               mkAnd (GHC.Base.map (fun '(SrcLoc.L l x) => SrcLoc.L l (simplify f x)) xs)
           | f, Or xs =>
               mkOr (GHC.Base.map (fun '(SrcLoc.L l x) => SrcLoc.L l (simplify f x)) xs)
           | f, Parens x => simplify f (SrcLoc.unLoc x)
           end.

Definition memberClauseAtoms {a} `{Unique.Uniquable a}
   : a -> Clause a -> bool :=
  fun x c => UniqSet.elementOfUniqSet x (clauseAtoms c).

Definition isTrue {a} : BooleanFormula a -> bool :=
  fun arg_0__ => match arg_0__ with | And nil => true | _ => false end.

Definition isUnsatisfied {a} `{GHC.Base.Eq_ a}
   : (a -> bool) -> BooleanFormula a -> option (BooleanFormula a) :=
  fun f bf =>
    let f' := fun x => if f x : bool then Some true else None in
    let bf' := simplify f' bf in if isTrue bf' : bool then None else Some bf'.

Definition isFalse {a} : BooleanFormula a -> bool :=
  fun arg_0__ => match arg_0__ with | Or nil => true | _ => false end.

Definition impliesAtom {a} `{GHC.Base.Eq_ a} : BooleanFormula a -> a -> bool :=
  fix impliesAtom arg_0__ arg_1__
        := match arg_0__, arg_1__ with
           | Var x, y => x GHC.Base.== y
           | And xs, y => Data.Foldable.any (fun x => impliesAtom (SrcLoc.unLoc x) y) xs
           | Or xs, y => Data.Foldable.all (fun x => impliesAtom (SrcLoc.unLoc x) y) xs
           | Parens x, y => impliesAtom (SrcLoc.unLoc x) y
           end.

Definition extendClauseAtoms {a} `{Unique.Uniquable a}
   : Clause a -> a -> Clause a :=
  fun c x =>
    let 'Mk_Clause clauseAtoms_0__ clauseExprs_1__ := c in
    Mk_Clause (UniqSet.addOneToUniqSet (clauseAtoms c) x) clauseExprs_1__.

Definition implies {a} `{Unique.Uniquable a}
   : BooleanFormula a -> BooleanFormula a -> bool :=
  fun e1 e2 =>
    let go {a} `{Unique.Uniquable a} : Clause a -> Clause a -> bool :=
      GHC.DeferredFix.deferredFix2 (fun go arg_0__ arg_1__ =>
                                      match arg_0__, arg_1__ with
                                      | (Mk_Clause _ (cons hyp hyps) as l), r =>
                                          match hyp with
                                          | Var x =>
                                              if memberClauseAtoms x r : bool then true else
                                              go (let 'Mk_Clause clauseAtoms_2__ clauseExprs_3__ := (extendClauseAtoms l
                                                                                x) in
                                                  Mk_Clause clauseAtoms_2__ hyps) r
                                          | Parens hyp' =>
                                              go (let 'Mk_Clause clauseAtoms_9__ clauseExprs_10__ := l in
                                                  Mk_Clause clauseAtoms_9__ (cons (SrcLoc.unLoc hyp') hyps)) r
                                          | And hyps' =>
                                              go (let 'Mk_Clause clauseAtoms_14__ clauseExprs_15__ := l in
                                                  Mk_Clause clauseAtoms_14__ (Coq.Init.Datatypes.app (GHC.Base.map
                                                                                SrcLoc.unLoc
                                                                                hyps') hyps)) r
                                          | Or hyps' =>
                                              Data.Foldable.all (fun hyp' =>
                                                                   go (let 'Mk_Clause clauseAtoms_19__
                                                                          clauseExprs_20__ := l in
                                                                       Mk_Clause clauseAtoms_19__ (cons (SrcLoc.unLoc
                                                                                hyp') hyps)) r)
                                              hyps'
                                          end
                                      | l, (Mk_Clause _ (cons con cons_) as r) =>
                                          match con with
                                          | Var x =>
                                              if memberClauseAtoms x l : bool then true else
                                              go l (let 'Mk_Clause clauseAtoms_27__ clauseExprs_28__ :=
                                                      (extendClauseAtoms r x) in
                                                    Mk_Clause clauseAtoms_27__ cons_)
                                          | Parens con' =>
                                              go l (let 'Mk_Clause clauseAtoms_34__ clauseExprs_35__ := r in
                                                    Mk_Clause clauseAtoms_34__ (cons (SrcLoc.unLoc con') cons_))
                                          | And cons' =>
                                              Data.Foldable.all (fun con' =>
                                                                   go l (let 'Mk_Clause clauseAtoms_39__
                                                                            clauseExprs_40__ := r in
                                                                         Mk_Clause clauseAtoms_39__ (cons (SrcLoc.unLoc
                                                                                con')
                                                                                cons_))) cons'
                                          | Or cons' =>
                                              go l (let 'Mk_Clause clauseAtoms_45__ clauseExprs_46__ := r in
                                                    Mk_Clause clauseAtoms_45__ (Coq.Init.Datatypes.app (GHC.Base.map
                                                                                SrcLoc.unLoc
                                                                                cons') cons_))
                                          end
                                      | _, _ => false
                                      end) in
    go (Mk_Clause UniqSet.emptyUniqSet (cons e1 nil)) (Mk_Clause
                                                       UniqSet.emptyUniqSet (cons e2 nil)).

Definition eval {a} : (a -> bool) -> BooleanFormula a -> bool :=
  fix eval arg_0__ arg_1__
        := match arg_0__, arg_1__ with
           | f, Var x => f x
           | f, And xs => Data.Foldable.all (eval f GHC.Base.∘ SrcLoc.unLoc) xs
           | f, Or xs => Data.Foldable.any (eval f GHC.Base.∘ SrcLoc.unLoc) xs
           | f, Parens x => eval f (SrcLoc.unLoc x)
           end.

Local Definition Eq___BooleanFormula_op_zeze__ {inst_a} `{GHC.Base.Eq_ inst_a}
   : BooleanFormula inst_a -> BooleanFormula inst_a -> bool :=
  fun arg_0__ arg_1__ =>
    match arg_0__, arg_1__ with
    | Var a1, Var b1 => ((a1 GHC.Base.== b1))
    | And a1, And b1 => ((a1 GHC.Base.== b1))
    | Or a1, Or b1 => ((a1 GHC.Base.== b1))
    | Parens a1, Parens b1 => ((a1 GHC.Base.== b1))
    | _, _ => false
    end.

Local Definition Eq___BooleanFormula_op_zsze__ {inst_a} `{GHC.Base.Eq_ inst_a}
   : BooleanFormula inst_a -> BooleanFormula inst_a -> bool :=
  fun x y => negb (Eq___BooleanFormula_op_zeze__ x y).

Program Instance Eq___BooleanFormula {a} `{GHC.Base.Eq_ a}
   : GHC.Base.Eq_ (BooleanFormula a) :=
  fun _ k__ =>
    k__ {| GHC.Base.op_zeze____ := Eq___BooleanFormula_op_zeze__ ;
           GHC.Base.op_zsze____ := Eq___BooleanFormula_op_zsze__ |}.

(* Skipping all instances of class `Data.Data.Data', including
   `BooleanFormula.Data__BooleanFormula' *)

Local Definition Functor__BooleanFormula_fmap {a} {b}
   : (a -> b) -> BooleanFormula a -> BooleanFormula b :=
  BooleanFormula_fmap.

Fixpoint Functor__BooleanFormula_op_zlzd__ {a} {b} (arg_0__ : a) (arg_1__
                                             : BooleanFormula b) : BooleanFormula a
           := match arg_0__, arg_1__ with
              | z, Var a1 => Var ((fun b1 => z) a1)
              | z, And a1 =>
                  And (GHC.Base.fmap (GHC.Base.fmap (Functor__BooleanFormula_op_zlzd__ z)) a1)
              | z, Or a1 =>
                  Or (GHC.Base.fmap (GHC.Base.fmap (Functor__BooleanFormula_op_zlzd__ z)) a1)
              | z, Parens a1 =>
                  Parens (GHC.Base.fmap (Functor__BooleanFormula_op_zlzd__ z) a1)
              end.

Program Instance Functor__BooleanFormula : GHC.Base.Functor BooleanFormula :=
  fun _ k__ =>
    k__ {| GHC.Base.fmap__ := fun {a} {b} => Functor__BooleanFormula_fmap ;
           GHC.Base.op_zlzd____ := fun {a} {b} => Functor__BooleanFormula_op_zlzd__ |}.

Local Definition Foldable__BooleanFormula_foldMap {m} {a} `{_
   : GHC.Base.Monoid m}
   : (a -> m) -> BooleanFormula a -> m :=
  BooleanFormula_foldMap.

Local Definition Foldable__BooleanFormula_fold
   : forall {m}, forall `{GHC.Base.Monoid m}, BooleanFormula m -> m :=
  fun {m} `{GHC.Base.Monoid m} => Foldable__BooleanFormula_foldMap GHC.Base.id.

Local Definition Foldable__BooleanFormula_foldl
   : forall {b} {a}, (b -> a -> b) -> b -> BooleanFormula a -> b :=
  fun {b} {a} =>
    fun f z t =>
      Data.SemigroupInternal.appEndo (Data.SemigroupInternal.getDual
                                      (Foldable__BooleanFormula_foldMap (Data.SemigroupInternal.Mk_Dual GHC.Base.∘
                                                                         (Data.SemigroupInternal.Mk_Endo GHC.Base.∘
                                                                          GHC.Base.flip f)) t)) z.

Local Definition Foldable__BooleanFormula_foldr {a} {b}
   : (a -> b -> b) -> b -> BooleanFormula a -> b :=
  BooleanFormula_foldr.

Local Definition Foldable__BooleanFormula_foldl'
   : forall {b} {a}, (b -> a -> b) -> b -> BooleanFormula a -> b :=
  fun {b} {a} =>
    fun f z0 xs =>
      let f' := fun x k z => k (f z x) in
      Foldable__BooleanFormula_foldr f' GHC.Base.id xs z0.

Local Definition Foldable__BooleanFormula_foldr'
   : forall {a} {b}, (a -> b -> b) -> b -> BooleanFormula a -> b :=
  fun {a} {b} =>
    fun f z0 xs =>
      let f' := fun k x z => k (f x z) in
      Foldable__BooleanFormula_foldl f' GHC.Base.id xs z0.

Local Definition Foldable__BooleanFormula_length
   : forall {a}, BooleanFormula a -> GHC.Num.Int :=
  fun {a} =>
    Foldable__BooleanFormula_foldl' (fun arg_0__ arg_1__ =>
                                       match arg_0__, arg_1__ with
                                       | c, _ => c GHC.Num.+ #1
                                       end) #0.

Fixpoint Foldable__BooleanFormula_null {a} (arg_0__ : BooleanFormula a) : bool
           := match arg_0__ with
              | Var _ => false
              | And a1 =>
                  Data.Foldable.all (Data.Foldable.all Foldable__BooleanFormula_null) a1
              | Or a1 =>
                  Data.Foldable.all (Data.Foldable.all Foldable__BooleanFormula_null) a1
              | Parens a1 => Data.Foldable.all Foldable__BooleanFormula_null a1
              end.

Local Definition Foldable__BooleanFormula_product
   : forall {a}, forall `{GHC.Num.Num a}, BooleanFormula a -> a :=
  fun {a} `{GHC.Num.Num a} =>
    Coq.Program.Basics.compose Data.SemigroupInternal.getProduct
                               (Foldable__BooleanFormula_foldMap Data.SemigroupInternal.Mk_Product).

Local Definition Foldable__BooleanFormula_sum
   : forall {a}, forall `{GHC.Num.Num a}, BooleanFormula a -> a :=
  fun {a} `{GHC.Num.Num a} =>
    Coq.Program.Basics.compose Data.SemigroupInternal.getSum
                               (Foldable__BooleanFormula_foldMap Data.SemigroupInternal.Mk_Sum).

Local Definition Foldable__BooleanFormula_toList
   : forall {a}, BooleanFormula a -> list a :=
  fun {a} =>
    fun t =>
      GHC.Base.build' (fun _ => (fun c n => Foldable__BooleanFormula_foldr c n t)).

Program Instance Foldable__BooleanFormula
   : Data.Foldable.Foldable BooleanFormula :=
  fun _ k__ =>
    k__ {| Data.Foldable.fold__ := fun {m} `{GHC.Base.Monoid m} =>
             Foldable__BooleanFormula_fold ;
           Data.Foldable.foldMap__ := fun {m} {a} `{GHC.Base.Monoid m} =>
             Foldable__BooleanFormula_foldMap ;
           Data.Foldable.foldl__ := fun {b} {a} => Foldable__BooleanFormula_foldl ;
           Data.Foldable.foldl'__ := fun {b} {a} => Foldable__BooleanFormula_foldl' ;
           Data.Foldable.foldr__ := fun {a} {b} => Foldable__BooleanFormula_foldr ;
           Data.Foldable.foldr'__ := fun {a} {b} => Foldable__BooleanFormula_foldr' ;
           Data.Foldable.length__ := fun {a} => Foldable__BooleanFormula_length ;
           Data.Foldable.null__ := fun {a} => Foldable__BooleanFormula_null ;
           Data.Foldable.product__ := fun {a} `{GHC.Num.Num a} =>
             Foldable__BooleanFormula_product ;
           Data.Foldable.sum__ := fun {a} `{GHC.Num.Num a} =>
             Foldable__BooleanFormula_sum ;
           Data.Foldable.toList__ := fun {a} => Foldable__BooleanFormula_toList |}.

Local Definition Traversable__BooleanFormula_traverse {f} {a} {b} `{_
   : GHC.Base.Applicative f}
   : (a -> f b) -> BooleanFormula a -> f (BooleanFormula b) :=
  BooleanFormula_traverse.

Local Definition Traversable__BooleanFormula_mapM
   : forall {m} {a} {b},
     forall `{GHC.Base.Monad m},
     (a -> m b) -> BooleanFormula a -> m (BooleanFormula b) :=
  fun {m} {a} {b} `{GHC.Base.Monad m} => Traversable__BooleanFormula_traverse.

Local Definition Traversable__BooleanFormula_sequenceA
   : forall {f} {a},
     forall `{GHC.Base.Applicative f},
     BooleanFormula (f a) -> f (BooleanFormula a) :=
  fun {f} {a} `{GHC.Base.Applicative f} =>
    Traversable__BooleanFormula_traverse GHC.Base.id.

Local Definition Traversable__BooleanFormula_sequence
   : forall {m} {a},
     forall `{GHC.Base.Monad m}, BooleanFormula (m a) -> m (BooleanFormula a) :=
  fun {m} {a} `{GHC.Base.Monad m} => Traversable__BooleanFormula_sequenceA.

Program Instance Traversable__BooleanFormula
   : Data.Traversable.Traversable BooleanFormula :=
  fun _ k__ =>
    k__ {| Data.Traversable.mapM__ := fun {m} {a} {b} `{GHC.Base.Monad m} =>
             Traversable__BooleanFormula_mapM ;
           Data.Traversable.sequence__ := fun {m} {a} `{GHC.Base.Monad m} =>
             Traversable__BooleanFormula_sequence ;
           Data.Traversable.sequenceA__ := fun {f} {a} `{GHC.Base.Applicative f} =>
             Traversable__BooleanFormula_sequenceA ;
           Data.Traversable.traverse__ := fun {f} {a} {b} `{GHC.Base.Applicative f} =>
             Traversable__BooleanFormula_traverse |}.

(* Skipping all instances of class `Binary.Binary', including
   `BooleanFormula.Binary__BooleanFormula' *)

(* Skipping all instances of class `Outputable.Outputable', including
   `BooleanFormula.Outputable__BooleanFormula' *)

(* External variables:
     BooleanFormula_fmap BooleanFormula_foldMap BooleanFormula_foldr
     BooleanFormula_traverse None Some bool cons false list negb nil option true
     Coq.Init.Datatypes.app Coq.Program.Basics.compose Data.Foldable.Foldable
     Data.Foldable.all Data.Foldable.any Data.Foldable.foldMap__ Data.Foldable.fold__
     Data.Foldable.foldl'__ Data.Foldable.foldl__ Data.Foldable.foldr'__
     Data.Foldable.foldr__ Data.Foldable.length__ Data.Foldable.null__
     Data.Foldable.product__ Data.Foldable.sum__ Data.Foldable.toList__
     Data.Maybe.maybe Data.OldList.nub Data.SemigroupInternal.Mk_Dual
     Data.SemigroupInternal.Mk_Endo Data.SemigroupInternal.Mk_Product
     Data.SemigroupInternal.Mk_Sum Data.SemigroupInternal.appEndo
     Data.SemigroupInternal.getDual Data.SemigroupInternal.getProduct
     Data.SemigroupInternal.getSum Data.Traversable.Traversable
     Data.Traversable.mapM__ Data.Traversable.sequenceA__ Data.Traversable.sequence__
     Data.Traversable.traverse__ GHC.Base.Applicative GHC.Base.Eq_ GHC.Base.Functor
     GHC.Base.Monad GHC.Base.Monoid GHC.Base.build' GHC.Base.flip GHC.Base.fmap
     GHC.Base.fmap__ GHC.Base.id GHC.Base.map GHC.Base.op_z2218U__ GHC.Base.op_zeze__
     GHC.Base.op_zeze____ GHC.Base.op_zlzd____ GHC.Base.op_zsze____
     GHC.DeferredFix.deferredFix2 GHC.Num.Int GHC.Num.Num GHC.Num.fromInteger
     GHC.Num.op_zp__ MonadUtils.concatMapM SrcLoc.L SrcLoc.Located SrcLoc.unLoc
     UniqSet.UniqSet UniqSet.addOneToUniqSet UniqSet.elementOfUniqSet
     UniqSet.emptyUniqSet Unique.Uniquable
*)

author: DavidFHCh

repo: Tesis-FTW

save_path: github-repos/coq/DavidFHCh-Tesis-FTW


text:
(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** Type-checking Linear code. *)

Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Globalenvs.
Require Import Memory.
Require Import Events.
Require Import Op.
Require Import Machregs.
Require Import Locations.
Require Import Conventions.
Require Import LTL.
Require Import Linear.

(** The rules are presented as boolean-valued functions so that we
  get an executable type-checker for free. *)

Section WT_INSTR.

Variable funct: function.

Definition slot_valid (sl: slot) (ofs: Z) (ty: typ): bool :=
  match sl with
  | Local => zle 0 ofs
  | Outgoing => zle 0 ofs
  | Incoming => In_dec Loc.eq (S Incoming ofs ty) (loc_parameters funct.(fn_sig))
  end &&
  match ty with Tlong => false | _ => true end.

Definition slot_writable (sl: slot) : bool :=
  match sl with
  | Local => true
  | Outgoing => true
  | Incoming => false
  end.

Definition loc_valid (l: loc) : bool :=
  match l with
  | R r => true
  | S Local ofs ty => slot_valid Local ofs ty
  | S _ _ _ => false
  end.

Definition wt_instr (i: instruction) : bool :=
  match i with
  | Lgetstack sl ofs ty r =>
      subtype ty (mreg_type r) && slot_valid sl ofs ty
  | Lsetstack r sl ofs ty =>
      slot_valid sl ofs ty && slot_writable sl
  | Lop op args res =>
      match is_move_operation op args with
      | Some arg =>
          subtype (mreg_type arg) (mreg_type res)
      | None =>
          let (targs, tres) := type_of_operation op in
          subtype tres (mreg_type res)
      end
  | Lload chunk addr args dst =>
      subtype (type_of_chunk chunk) (mreg_type dst)
  | Ltailcall sg ros =>
      zeq (size_arguments sg) 0
  | Lbuiltin ef args res =>
      subtype_list (proj_sig_res' (builtin_sig ef)) (map mreg_type res)
  | Lannot ef args =>
      forallb loc_valid args
  | _ =>
      true
  end.

End WT_INSTR.

Definition wt_code (f: function) (c: code) : bool :=
  forallb (wt_instr f) c.

Definition wt_function (f: function) : bool :=
  wt_code f f.(fn_code).

(** Typing the run-time state. *)

Definition wt_locset (ls: locset) : Prop :=
  forall l, Val.has_type (ls l) (Loc.type l).

Lemma wt_setreg:
  forall ls r v,
  Val.has_type v (mreg_type r) -> wt_locset ls -> wt_locset (Locmap.set (R r) v ls).
Proof.
  intros; red; intros.
  unfold Locmap.set.
  destruct (Loc.eq (R r) l).
  subst l; auto.
  destruct (Loc.diff_dec (R r) l). auto. red. auto.
Qed.

Lemma wt_setstack:
  forall ls sl ofs ty v,
  wt_locset ls -> wt_locset (Locmap.set (S sl ofs ty) v ls).
Proof.
  intros; red; intros.
  unfold Locmap.set.
  destruct (Loc.eq (S sl ofs ty) l).
  subst l. simpl.
  generalize (Val.load_result_type (chunk_of_type ty) v).
  replace (type_of_chunk (chunk_of_type ty)) with ty. auto.
  destruct ty; reflexivity.
  destruct (Loc.diff_dec (S sl ofs ty) l). auto. red. auto.
Qed.

Lemma wt_undef_regs:
  forall rs ls, wt_locset ls -> wt_locset (undef_regs rs ls).
Proof.
  induction rs; simpl; intros. auto. apply wt_setreg; auto. red; auto.
Qed.

Lemma wt_call_regs:
  forall ls, wt_locset ls -> wt_locset (call_regs ls).
Proof.
  intros; red; intros. unfold call_regs. destruct l. auto.
  destruct sl.
  red; auto.
  change (Loc.type (S Incoming pos ty)) with (Loc.type (S Outgoing pos ty)). auto.
  red; auto.
Qed.

Lemma wt_return_regs:
  forall caller callee,
  wt_locset caller -> wt_locset callee -> wt_locset (return_regs caller callee).
Proof.
  intros; red; intros.
  unfold return_regs. destruct l; auto.
  destruct (in_dec mreg_eq r destroyed_at_call); auto.
Qed.

Lemma wt_init:
  wt_locset (Locmap.init Vundef).
Proof.
  red; intros. unfold Locmap.init. red; auto.
Qed.

Lemma wt_setlist:
  forall vl rl rs,
  Val.has_type_list vl (map mreg_type rl) ->
  wt_locset rs ->
  wt_locset (Locmap.setlist (map R rl) vl rs).
Proof.
  induction vl; destruct rl; simpl; intros; try contradiction.
  auto.
  destruct H. apply IHvl; auto. apply wt_setreg; auto.
Qed.

Lemma wt_find_label:
  forall f lbl c,
  wt_function f = true ->
  find_label lbl f.(fn_code) = Some c ->
  wt_code f c = true.
Proof.
  unfold wt_function; intros until c. generalize (fn_code f). induction c0; simpl; intros.
  discriminate.
  InvBooleans. destruct (is_label lbl a).
  congruence.
  auto.
Qed.

(** Soundness of the type system *)

Definition wt_fundef (fd: fundef) :=
  match fd with
  | Internal f => wt_function f = true
  | External ef => True
  end.

Inductive wt_callstack: list stackframe -> Prop :=
  | wt_callstack_nil:
      wt_callstack nil
  | wt_callstack_cons: forall f sp rs c s
        (WTSTK: wt_callstack s)
        (WTF: wt_function f = true)
        (WTC: wt_code f c = true)
        (WTRS: wt_locset rs),
      wt_callstack (Stackframe f sp rs c :: s).

Lemma wt_parent_locset:
  forall s, wt_callstack s -> wt_locset (parent_locset s).
Proof.
  induction 1; simpl.
- apply wt_init.
- auto.
Qed.

Inductive wt_state: state * mem -> Prop :=
  | wt_regular_state: forall s f sp c rs m
        (WTSTK: wt_callstack s )
        (WTF: wt_function f = true)
        (WTC: wt_code f c = true)
        (WTRS: wt_locset rs),
      wt_state (State s f sp c rs, m)
  | wt_call_state: forall s fd rs m
        (WTSTK: wt_callstack s)
        (WTFD: wt_fundef fd)
        (WTRS: wt_locset rs),
      wt_state (Callstate s fd rs, m)
  | wt_return_state: forall s rs m
        (WTSTK: wt_callstack s)
        (WTRS: wt_locset rs),
      wt_state (Returnstate s rs, m).

(** Preservation of state typing by transitions *)

Section SOUNDNESS.

Variable prog: program.
Let ge := Genv.globalenv prog.

Hypothesis wt_prog:
  forall i fd, In (i, Gfun fd) prog.(prog_defs) -> wt_fundef fd.

Lemma wt_find_function:
  forall ros rs f, find_function ge ros rs = Some f -> wt_fundef f.
Proof.
  intros.
  assert (X: exists i, In (i, Gfun f) prog.(prog_defs)).
  {
    destruct ros as [r | s]; simpl in H.
    eapply Genv.find_funct_inversion; eauto.
    destruct (Genv.find_symbol ge s) as [b|]; try discriminate.
    eapply Genv.find_funct_ptr_inversion; eauto.
  }
  destruct X as [i IN]. eapply wt_prog; eauto.
Qed.

Theorem step_type_preservation:
  forall S1 t S2, step ge S1 t S2 -> wt_state S1 -> wt_state S2.
Proof.
  induction 1; intros WTS; inv WTS.
- (* getstack *)
  simpl in *; InvBooleans.
  econstructor; eauto.
  eapply wt_setreg; eauto. eapply Val.has_subtype; eauto. apply WTRS.
  apply wt_undef_regs; auto.
- (* setstack *)
  simpl in *; InvBooleans.
  econstructor; eauto.
  apply wt_setstack. apply wt_undef_regs; auto.
- (* op *)
  simpl in *. destruct (is_move_operation op args) as [src | ] eqn:ISMOVE.
  + (* move *)
    InvBooleans. exploit is_move_operation_correct; eauto. intros [EQ1 EQ2]; subst.
    simpl in H. inv H.
    econstructor; eauto. apply wt_setreg. eapply Val.has_subtype; eauto. apply WTRS.
    apply wt_undef_regs; auto.
  + (* other ops *)
    destruct (type_of_operation op) as [ty_args ty_res] eqn:TYOP. InvBooleans.
    econstructor; eauto.
    apply wt_setreg; auto. eapply Val.has_subtype; eauto.
    change ty_res with (snd (ty_args, ty_res)). rewrite <- TYOP. eapply type_of_operation_sound; eauto.
    red; intros; subst op. simpl in ISMOVE.
    destruct args; try discriminate. destruct args; discriminate.
    apply wt_undef_regs; auto.
- (* load *)
  simpl in *; InvBooleans.
  econstructor; eauto.
  apply wt_setreg. eapply Val.has_subtype; eauto.
  destruct a; simpl in H0; try discriminate. eapply Mem.load_type; eauto.
  apply wt_undef_regs; auto.
- (* store *)
  simpl in *; InvBooleans.
  econstructor. eauto. eauto. eauto.
  apply wt_undef_regs; auto.
- (* call *)
  simpl in *; InvBooleans.
  econstructor; eauto. econstructor; eauto.
  eapply wt_find_function; eauto.
- (* tailcall *)
  simpl in *; InvBooleans.
  econstructor; eauto.
  eapply wt_find_function; eauto.
  apply wt_return_regs; auto. apply wt_parent_locset; auto.
- (* builtin *)
  simpl in *; InvBooleans.
  econstructor; eauto.
  apply wt_setlist.
  eapply Val.has_subtype_list; eauto. eapply builtin_call_well_typed'; eauto.
  apply wt_undef_regs; auto.
- (* annot *)
  simpl in *; InvBooleans.
  econstructor; eauto.
- (* label *)
  simpl in *. econstructor; eauto.
- (* goto *)
  simpl in *. econstructor; eauto. eapply wt_find_label; eauto.
- (* cond branch, taken *)
  simpl in *. econstructor. auto. auto. eapply wt_find_label; eauto.
  apply wt_undef_regs; auto.
- (* cond branch, not taken *)
  simpl in *. econstructor. auto. auto. auto.
  apply wt_undef_regs; auto.
- (* jumptable *)
  simpl in *. econstructor. auto. auto. eapply wt_find_label; eauto.
  apply wt_undef_regs; auto.
- (* return *)
  simpl in *. InvBooleans.
  econstructor; eauto.
  apply wt_return_regs; auto. apply wt_parent_locset; auto.
- (* internal function *)
  simpl in WTFD.
  econstructor. eauto. eauto. eauto.
  apply wt_undef_regs. apply wt_call_regs. auto.
- (* external function *)
  econstructor. auto. apply wt_setlist; auto.
  eapply Val.has_subtype_list. apply loc_result_type. eapply external_call_well_typed'; eauto.
- (* return *)
  inv WTSTK. econstructor; eauto.
Qed.

Theorem wt_initial_state:
  forall S, initial_state prog S -> wt_state S.
Proof.
  induction 1. econstructor. constructor.
  unfold ge0 in H1. exploit Genv.find_funct_ptr_inversion; eauto.
  intros [id IN]. eapply wt_prog; eauto.
  apply wt_init.
Qed.

End SOUNDNESS.

(** Properties of well-typed states that are used in [Stackingproof]. *)

Lemma wt_state_getstack:
  forall s f sp sl ofs ty rd c rs m,
  wt_state (State s f sp (Lgetstack sl ofs ty rd :: c) rs, m) ->
  slot_valid f sl ofs ty = true.
Proof.
  intros. inv H. simpl in WTC; InvBooleans. auto.
Qed.

Lemma wt_state_setstack:
  forall s f sp sl ofs ty r c rs m,
  wt_state (State s f sp (Lsetstack r sl ofs ty :: c) rs, m) ->
  slot_valid f sl ofs ty = true /\ slot_writable sl = true.
Proof.
  intros. inv H. simpl in WTC; InvBooleans. intuition.
Qed.

Lemma wt_state_tailcall:
  forall s f sp sg ros c rs m,
  wt_state (State s f sp (Ltailcall sg ros :: c) rs, m) ->
  size_arguments sg = 0.
Proof.
  intros. inv H. simpl in WTC; InvBooleans. auto.
Qed.

Lemma wt_state_annot:
  forall s f sp ef args c rs m,
  wt_state (State s f sp (Lannot ef args :: c) rs, m) ->
  forallb (loc_valid f) args = true.
Proof.
  intros. inv H. simpl in WTC; InvBooleans. auto.
Qed.

Lemma wt_callstate_wt_regs:
  forall s f rs m,
  wt_state (Callstate s f rs, m) ->
  forall r, Val.has_type (rs (R r)) (mreg_type r).
Proof.
  intros. inv H. apply WTRS.
Qed.

author: robbertkrebbers

repo: compcert


text:
(* disc1.v  *)

Require Import List.
Fixpoint g_one (l : nat) : list bool :=
  match l with
  | 0 => nil
  | 1 => true::nil
  | S l' => g_one l' ++ false::nil
  end.

Lemma one_is_one_longer :
  forall (l : nat),
    0 < l -> g_one(S l) = g_one(l) ++ false::nil.
Proof.
  intros.
  simpl.
  apply Lt.lt_0_neq in H.
  destruct l.
  contradiction.
  reflexivity.
Restart.
(* We are smarter than this*)
 simpl => l; elim l => H ; last first; trivial.
 apply Lt.lt_0_neq in H.
 contradiction.
Qed.

Require Import ssreflect.
Lemma ssr_rules :
  forall (l : nat),
    0 < l -> g_one (S l) = g_one(l) ++ false::nil.
Proof.
by case=>//= /Lt.lt_0_neq //.
Qed.

From mathcomp Require Import ssrbool ssrnat.
(* Adds 0 <> 0 as hint *)
Lemma ssr_rules_overalles :
  forall (l : nat),
    0 < l -> g_one (S l) = g_one(l) ++ false :: nil.
Proof. by case. Qed.

author: germanD

repo: misc

save_path: github-repos/coq/germanD-misc