(*******************************************************************************)
(* Copyright 2020 Catherine Dubois, Alain Giorgetti and Nicolas Magaud         *)
(* Samovar - FEMTO-ST institute - I-cube                                       *)
(*******************************************************************************)

(*******************************************************************************)
(*      This file is distributed under the terms of the                        *)
(*       GNU Lesser General Public License Version 2.1                         *)
(*******************************************************************************)

(** Boolean functions corresponding to theorems in [map.v] *)

(* File: exec.v.

   Contents:
   1. Boolean functions corresponding to the preservation theorems in map.v.
   2. Boolean function for the (wrong) lemma of preservation of transitivity
      by sum. *)

Require Import Arith Arith.Even Omega List.
Require Import endofun permut operations trans map.

Set Implicit Arguments.

(** * Boolean functions corresponding to both preservation theorems *)

Open Scope bool_scope.

Definition isthmic_fun_transitiveb d1 (r1 : nat -> nat) d2 (r2 : nat -> nat) :=
if even_odd_dec d1 then
if even_odd_dec d2 then
if is_permutb d1 r1 && is_transitive_funb d1 r1 &&
 is_permutb d2 r2 && is_transitive_funb d2 r2 
then 
 is_transitive_funb (S (S (d1 + d2))) (isthmic_fun d1 r1 d2 r2)
else true else true else true.
 
Definition non_isthmic_fun_transitiveb d (r : nat -> nat) k (k_le_d : k <= d) :=
if even_odd_dec d then
if is_permutb d r && is_transitive_funb d r
then
 is_transitive_funb (S (S d)) (@non_isthmic_fun d r k k_le_d)
else true else true.

(** * Boolean function for a wrong lemma

   [Lemma sum_transitive d1 r1 d2 r2 (H1 : even d1) (H2 : even d2) :
    is_transitive_fun d1 r1 -> is_transitive_fun d2 r2 ->  
    is_transitive_fun (d1 + d2) (sum_fun d1 r1 d2 r2).] *)

Definition sum_transitiveb d1 r1 d2 r2 :=
if even_odd_dec d1 then
if even_odd_dec d2 then
if is_permutb d1 r1 && is_transitive_funb d1 r1 &&
 is_permutb d2 r2 && is_transitive_funb d2 r2 
then 
 is_transitive_funb (d1 + d2) (sum_fun d1 r1 d2 r2)
else true else true else true.