The Coq mailing list

["Jael E. Kriener" <jek26 AT kent.ac.uk>]

Thanks for the quick reply, Adam!

I attached the wrong file the second time around - I'm very sorry! This 
one is self-contained and useful. Sorry again.

Is it possible that using 8.4beta might make this trivial?

Jael


On 20/02/12 20:26, Adam Chlipala wrote:
> On 02/20/2012 12:52 PM, J.E.Kriener wrote:
> > I've defined a function over (dependent) types using Fixpoint and 
> > refine. Now I'm trying to prove something about it. So I'm trying to 
> > apply it to some specific arguments and look at the result. But I 
> > seem to be unable to simply do that:
> >
> >          'simpl' won't change a thing,
> >          neither will 'unfold ; simpl'.
>
> [simpl] seems to do everything I expect in your simplified example.  
> What about the behavior surprises you?
>
> Your example is odd, in that you use [Fixpoint] to define a 
> non-recursive function.  Keep in mind that applications of recursive 
> functions can only simplify when the top-level structure of the 
> recursive argument is known.  Perhaps an annotation to indicate which 
> argument is recursive would help you somewhere.
>
> But I would just use [Definition] instead of [Fixpoint], in any case.
>
> P.S.: The example still imports CoLoR modules, though it doesn't use 
> them later.

Require Import Program.Basics.
Require Import ZArith.
Require Import Morphisms Setoid.
Require Import Setoid.
Require Import Equalities.
Require Import Eqdep.
Require Import Program.Equality.
Require Import Recdef.
Require Import List.
Require Import Bool.

(*Add Rec LoadPath "~/Work/Research/Coq-Proofs/libraries/ubuntu/color/trunk/color" as CoLoR.
Require Import CoLoR.Util.Vector.VecEq.
Require Import CoLoR.Util.Vector.VecUtil.
*)
Inductive vector (A : Type) : nat -> Type :=
    Vnil : vector A 0
  | Vcons : A -> forall n : nat, vector A n -> vector A (S n).

Parameter eq_vec : forall (A : Type) (n : nat), vector A n -> vector A n -> Prop.
Parameter eq_vec_refl : forall A n v,  eq_vec A n  v v.
Parameter eq_vec_sym : forall A n v v', eq_vec A n  v v' -> eq_vec A n v' v.
Parameter eq_vec_trans : forall A n u v w, eq_vec A n u v -> eq_vec A n v w -> eq_vec A n u w.

Section EqVec.
Parameter A : Type.
Parameter n : nat.

Global Instance EqVec : Equivalence (eq_vec A n).
Proof.
  split ; [unfold Reflexive ; apply eq_vec_refl | unfold Symmetric ; apply eq_vec_sym | unfold Transitive ; apply eq_vec_trans].
Defined.
End EqVec.
  
Axiom eq_vec_cons
     : forall (A : Type) (eqA : A -> A -> Prop) (x x' : A) 
         (n : nat) (v v' : vector A n),
       eq_vec A (S n) (Vcons A x n v) (Vcons A  x' n  v') <-> eqA x x' /\ eq_vec A n v v'.

Axiom V0_eq 
     : forall (A : Type) (v : vector A 0), v = Vnil A.

Axiom VSn_inv
     : forall (A : Type) (n : nat) (v : vector A (S n)),
       exists x : A, exists w : vector A n, v = Vcons A  x n w.

Instance Eq_nat_E : Equivalence (eq_nat).

   split ; [unfold Reflexive | unfold Symmetric | unfold Transitive ] .
   apply eq_nat_refl.
SearchAbout eq_nat.  
    induction x ; induction y ; intros.
    apply eq_nat_refl.
    inversion H.
    inversion H.
    simpl.
    apply IHx.
    simpl in H.
    assumption.

    induction x ; induction y ; induction z ; intros 
    ; try inversion H ; try inversion H0.
    apply eq_nat_refl.
    simpl in *.
    apply IHx with (y := y) ; assumption.
Qed.




(* ==================== TACTICS ====================== *)
Ltac andb_simpl := 
  match goal with
    | [ H : ?b1 && ?b2 = true |- _]
      => symmetry in H ; apply andb_true_eq in H ; destruct H
    | [ H : true = ?b |- _]
      => symmetry in H
    | [ |- ?b1 && ?b2 = true ]
      => apply andb_true_iff ; split
  end ; 
  try andb_simpl.

Ltac eq_induction_solv :=
  match goal with
    | [ A : forall x, ?beq ?a x = true -> ?eq ?a x , B : ?beq ?a ?b = true  |- ?eq ?a ?b]
      => apply A ; assumption
    | [A : forall x, ?eq ?a x -> ?beq ?a x = true, B: ?eq ?a ?b |- ?beq ?a ?b = true]
      => apply A ; assumption
  end.


(* == Variables & Var_Vecs == *)
Definition var_ident := nat.
Definition eq_var_ident : var_ident -> var_ident -> Prop := eq_nat.
Definition eq_var_ident_dec: forall (x y: var_ident), {x=y}+{x<>y} := eq_nat_dec.
Definition beq_var_ident := beq_nat.

Instance Beq_var_ident_Proper : Proper ( eq_var_ident ==> eq_var_ident ==> @eq bool) (beq_var_ident).
   intros a b A c d C.
   depind a.
   depind c.
   destruct b.
   destruct d.
   reflexivity.
   inversion C.
   inversion A.
   destruct b.
   destruct d.
   inversion C.
   simpl.
   reflexivity.
   inversion A.
   destruct b.
   inversion A.
   destruct c.
   destruct d.
   simpl ; reflexivity.
   inversion C.
   destruct d.
   inversion C.
   simpl.
   apply IHa.
   apply A.
   apply C.
Qed.

Definition var_vec := vector var_ident.
Definition eq_var_vec : (forall {n}, var_vec n -> var_vec n -> Prop) := eq_vec  (var_ident)  . 
Fixpoint beq_var_vec {m n : nat} (v : var_vec m) (w : var_vec n) : bool :=
 match (v, w) with 
   | (Vnil , Vnil )                           => true
   | (Vcons a _ v' , Vcons b _ w') => (beq_var_ident a b) && (beq_var_vec v' w')
   | (_, _)                                      => false
end. 

Section var_vec_eq.

Variable n : nat.
Variable t : var_ident.

Global Instance Eq_var_vec_E : Equivalence (eq_var_vec n).
  split.
  unfold Reflexive.
  apply eq_vec_refl .

  unfold Symmetric.
  apply eq_vec_sym.

  unfold Transitive.
  apply eq_vec_trans.
Qed.

(*Global Instance Vnil_eq_var_vec_Proper  : Proper (eq_var_vec _) (@Vnil var_ident).
   split.
Qed.

Global Instance Vcons_eq_var_vec_Proper  (n : nat) (t : var_ident)  :  Proper (eq_var_vec n  ==> eq_var_vec (S n)) 
( @Vcons _ t n ).
  intros l l' H.
  unfold eq_var_vec.
  apply eq_vec_cons.
  split.
  reflexivity.
  assumption.
Qed.
*)
Global Instance Beq_var_vec_Proper :  Proper (eq_var_vec n ==> eq_var_vec n ==> @eq bool ) beq_var_vec.
   intros a b A c d C.
   depind a.
   unfold eq_var_vec in *.
   assert (B : b = Vnil (var_ident )).
   depind b.
   reflexivity.
   subst.
   
   depind c.
   assert (D : d = Vnil (var_ident)).
   depind d.
   reflexivity.
   subst.
   simpl.
   reflexivity.
   
   rename a0 into a'.
   depind b.
   rename b into b' ; rename a0 into b.
   clear IHb.
   apply (eq_vec_cons (var_ident) (eq_var_ident)) in A ; destruct A as [A A'].
   
   depind c.
   depind d.
   clear IHc.
   clear IHd.
   rename c into c' ; rename a0 into c ;
     rename d into d' ; rename a1 into d.
   apply (eq_vec_cons (var_ident) (eq_var_ident))  in C ; destruct C as [C C'].
   simpl.
   remember (beq_var_ident a c).
   destruct b0.
   
   rewrite C in Heqb0.
   rewrite <- A.
   rewrite <- Heqb0. 
   simpl.
   apply IHa ; try assumption.
   rewrite <- A ; rewrite <- C ; rewrite <- Heqb0 ; simpl.
   reflexivity.
Qed.

End var_vec_eq.


Axiom beq_var_vec_ok : forall {n : nat} (v  w: var_vec n) , 
  beq_var_vec v w = true <-> eq_var_vec _ v w. 

 (* ==================== DOMAINS ===================== *)
 (* ===  Abstract Domain - non-specified ! === *)
Parameter D : Type.
(*Definition D := t d.*)
Parameter eq_d : D -> D -> Prop.
Axiom eq_d_trans : forall d e f , eq_d d e -> eq_d e f -> eq_d d f.
Axiom eq_d_refl : forall d, eq_d d d.
Axiom eq_d_sym : forall d e, eq_d d e -> eq_d e d.
Instance Eq_d_E : Equivalence eq_d.
  split.
  unfold Reflexive ; apply eq_d_refl.
  unfold Symmetric ; apply eq_d_sym.
  unfold Transitive ; apply eq_d_trans.
Defined.
Parameter eq_d_dec : forall (d1 d2 : D), {eq_d d1 d2}+{~ eq_d d1 d2}.
Parameter beq_d : D -> D -> bool.
Axiom beq_d_iff : forall d e, eq_d d e <-> beq_d d e = true.

Instance Eq_d_Proper :  Proper (eq_d ==> flip eq_d ==> flip impl) eq_d.
  intros a b A c d C.
  unfold flip in * ; unfold impl ; intros.
  apply transitivity with (y := d) ; try assumption.
  apply transitivity with (y := b) ; try assumption.
Defined.


Parameter lt_d : D -> D -> Prop.
Parameter blt_d : D -> D -> bool.
Axiom blt_d_iff : forall d1 d2, lt_d d1 d2 <-> blt_d d1 d2 = true.
(* top and bottom elements for D with axioms *)
Parameter d_top : D.
Axiom d_top_top : forall d, blt_d d d_top = true.
Parameter d_bot : D.
Axiom  d_bot_bot : forall d, blt_d d_bot d = true.  

(* partial order on D *)
Axiom blt_d_refl : forall d e, beq_d d e = true -> blt_d d e = true.
Axiom blt_d_trans : forall d e f, blt_d d e = true -> blt_d e f = true -> blt_d d f = true.
Axiom blt_d_antisym : forall d e, blt_d d e = true -> blt_d e d = true -> beq_d d e = true.

Instance Blt_eq_Proper : Proper (eq_d ==> eq_d ==> @eq bool) blt_d.
  intros a b A c d C.
  remember (blt_d a c).
  rename b0 into h ; rename Heqb0 into H.
  destruct h.
  symmetry in H.
  symmetry in A.
  rewrite beq_d_iff in *.
  apply blt_d_refl in A.
  apply blt_d_refl in C.
  symmetry.
  apply blt_d_trans with (e := a) ; try assumption.
  apply blt_d_trans with (e := c) ; try assumption.

  remember (blt_d b d).
  rename b0 into g ; rename Heqb0 into G.
  destruct g ; try reflexivity.
  symmetry in H.
  symmetry in C.
  symmetry in G.
  rewrite beq_d_iff in *.
  apply blt_d_refl in A.
  apply blt_d_refl in C.
  assert (B: blt_d a d = true).
     apply blt_d_trans with (e := b) ; try assumption.
  assert (D: blt_d a c = true).
     apply blt_d_trans with (e := d) ; try assumption.
  rewrite H in D.
  assumption.
Defined.
  

Parameter join : D -> D -> D.
Axiom join_idem : forall d1, join d1 d1 = d1.
Axiom join_lt_true : forall d1 d2, (blt_d d1 d2 = true) -> (eq_d (join d1 d2) d2). 
Axiom join_commutative : forall d1 d2, eq_d (join d1 d2) (join d2 d1).

Parameter meet : D -> D -> D.
Axiom meet_idem : forall d1, meet d1 d1 = d1.
Axiom meet_lt_true : forall d1 d2, (blt_d d1 d2 = true) -> (eq_d (meet d1 d2) d1).
Axiom meet_commutative : forall d1 d2, eq_d (meet d1 d2) (meet d2 d1). 

Parameter e_proj : forall {n : nat},  var_vec n -> D -> D.
Axiom e_proj_eq_d_compat : forall {n : nat} (v : var_vec n) (a b : D), eq_d a b -> (eq_d (e_proj v a) (e_proj v b)).
Axiom e_proj_extensive : forall {n : nat} (v : var_vec n) (d1 : D), blt_d d1 (e_proj v d1) = true.


Instance E_proj_flip_impl_Proper {n : nat} (v : var_vec n) : Proper ( eq_d ==> eq_d ) (e_proj v).
  intros a b A.
  apply e_proj_eq_d_compat ; assumption.
Defined.

Axiom e_proj_monotone : forall {n : nat} (v : var_vec n) d1 d2, (blt_d d1 d2 = true) -> 
                                        (blt_d (e_proj v d1) (e_proj v d2) = true).  
Axiom e_proj_commutative : forall {n m : nat} (v1 : var_vec m) (v2 : var_vec n) d, eq_d (e_proj v1 (e_proj v2 d)) (e_proj v2 ( e_proj v1 d)).
Axiom weak_e_proj_meet_distr : forall {n : nat} (v : var_vec n) d1 d2, eq_d (meet (e_proj v d1) (e_proj v d2)) (e_proj v (meet d1 (e_proj v d2))).


(* ==================== SYNTAX ====================== *)


(*== Predicates ==*)
Definition pred_ident := nat.
Definition eq_pred_ident : pred_ident -> pred_ident -> Prop := eq_nat.
Definition eq_pred_ident_dec : forall (x y: pred_ident), {x=y}+{x<>y} := eq_nat_dec.
Definition beq_pred_ident := beq_nat.
Axiom beq_pred_ident_iff : forall x y, eq_pred_ident x y <-> beq_pred_ident x y = true.


Inductive Agent : Type :=
  | A_ask  : D -> Agent
  | A_conj : Agent -> Agent -> Agent
  | A_sum :  Agent -> Agent -> Agent
  | A_head : forall {n:nat}, pred_ident -> var_vec n -> Agent.


Inductive eq_agent : Agent -> Agent -> Prop :=
  | EqA_ask : forall d1 d2, eq_d d1 d2 
                                         -> eq_agent (A_ask d1) (A_ask d2)
  | EqA_conj : forall a1 a2 b1 b2, eq_agent a1 a2 
                                         -> eq_agent b1 b2 
                                         -> eq_agent (A_conj a1 b1) (A_conj a2 b2)
  | EqA_sum : forall a1 a2 b1 b2, eq_agent a1 a2 
                                         -> eq_agent b1 b2 
                                         -> eq_agent (A_sum a1 b1) (A_sum a2 b2)
  | EqA_head : forall p1 p2 n x1 x2, eq_pred_ident p1 p2 
                                         -> eq_var_vec n x1 x2 
                                         -> eq_agent (A_head p1 x1) (A_head p2 x2).

Parameter eq_agent_refl : Reflexive eq_agent.
Parameter eq_agent_sym : Symmetric eq_agent.
Parameter eq_agent_trans : Transitive eq_agent.
Instance Eq_Agent : Equivalence eq_agent.
Proof.
  constructor ; [apply eq_agent_refl | apply eq_agent_sym | apply eq_agent_trans].
Qed.

Fixpoint beq_agent (a b : Agent) : bool :=
  match (a,b) with
    | ((A_ask d), (A_ask e))      => beq_d d e
    | ((A_conj a b), (A_conj a' b'))  => beq_agent a a' && beq_agent b b'
    | ((A_sum a b), (A_sum a' b'))    => beq_agent a a' && beq_agent b b'
    | ((A_head n p x), (A_head n' p' x'))  => beq_pred_ident p p' && beq_nat n n' &&  beq_var_vec x x'
    | (_, _) => false
 end.

Lemma beq_agent_iff : forall a b, beq_agent a b = true <-> eq_agent a b.
Proof.
    intros ; split ; intros.
    depind a ; destruct b ; inversion H ; subst ; clear H ; try constructor ; repeat (andb_simpl) ; try eq_induction_solv.
    apply beq_d_iff ; assumption.
    apply beq_nat_true in H1 ; subst.
    constructor.
    apply beq_nat_true in H ; subst ; reflexivity.
    apply beq_var_vec_ok in H0 ; assumption.
    
    depind a ; destruct b ; depind H ; simpl ; try andb_simpl ; try eq_induction_solv.
    apply beq_d_iff in H ; auto.
    apply beq_pred_ident_iff ; auto.
    apply beq_nat_true_iff ; reflexivity.
    apply beq_var_vec_ok ; auto.
Qed.
   

Ltac beq_eq_solv :=
  match goal with
    (* eq_nat clauses - symmetry permutations*)
    | [H: beq_nat ?m ?n = true |- ?m = ?n]
      => apply beq_nat_true_iff in H ; assumption
    | [H: true = beq_nat ?m ?n |- ?m = ?n]
      => symmetry in H ; apply beq_nat_true_iff in H ; assumption
    | [H: beq_nat ?m ?n = true |- ?n = ?m]
      => apply beq_nat_true_iff in H ; symmetry ; assumption 
    | [H: true = beq_nat ?m ?n |- ?n = ?m]
      => symmetry in H ; apply beq_nat_true_iff in H ; symmetry ; assumption
    (* beq_nat clauses - symmetry permutations*)
    | [H: eq_nat ?m ?n |- beq_nat ?m ?n = true ]
      => apply beq_nat_true_iff ; assumption
    | [H: eq_nat ?m ?n |- true = beq_nat ?m ?n ]
      => symmetry ; apply beq_nat_true_iff ; assumption
    | [H: eq_nat ?n ?m |- beq_nat ?m ?n = true ]
      => apply beq_nat_true_iff ; symmetry ; assumption 
    | [H: eq_nat ?n ?m |- true = beq_nat ?m ?n ]
      => symmetry ; apply beq_nat_true_iff ; assumption
    | [ |- beq_nat ?n ?n = true ]
      => apply beq_nat_true_iff ; reflexivity

    (* eq_pred_ident clauses - symmetry permutations*)
    | [H: beq_pred_ident ?m ?n = true |- eq_pred_ident ?m ?n]
      => apply beq_pred_ident_iff in H ; assumption
    | [H: true = beq_pred_ident ?m ?n |- eq_pred_ident ?m ?n]
      => symmetry in H ; apply beq_pred_ident_iff in H ; assumption
    | [H: beq_pred_ident ?m ?n = true |- eq_pred_ident ?n ?m]
      => apply beq_pred_ident_iff in H ; symmetry ; assumption 
    | [H: true = beq_pred_ident ?m ?n |- eq_pred_ident ?n ?m]
      => symmetry in H ; apply beq_pred_ident_iff in H ; symmetry ; assumption
    (* beq_pred_ident clauses - symmetry permutations*)
    | [H: eq_pred_ident ?m ?n |- beq_pred_ident ?m ?n = true ]
      => apply beq_pred_ident_iff ; assumption
    | [H:  eq_pred_ident ?m ?n |- true = beq_pred_ident ?m ?n]
      => symmetry ; apply beq_pred_ident_iff ; assumption
    | [H: eq_pred_ident ?n ?m |- beq_pred_ident ?m ?n = true ] 
      => apply beq_pred_ident_iff ; symmetry ; assumption 
    | [H: eq_pred_ident ?n ?m |- true = beq_pred_ident ?m ?n ]
      => symmetry in H ; apply beq_pred_ident_iff in H ; assumption

    (* eq_d clauses - symmetry permutations*)
    | [H: beq_d ?m ?n = true |- eq_d ?m ?n]
      => apply beq_d_iff in H ; assumption
    | [H: true = beq_d ?m ?n |- eq_d ?m ?n]
      => symmetry in H ; apply beq_d_iff in H ; assumption
    | [H: beq_d ?m ?n = true |- eq_d ?n ?m]
      => apply beq_d_iff in H ; symmetry ; assumption 
    | [H: true = beq_d ?m ?n |- eq_d ?n ?m]
      => symmetry in H ; apply beq_d_iff in H ; symmetry ; assumption
    (* beq_d clauses - symmetry permutations*)
    | [H: eq_d ?m ?n |- beq_d ?m ?n = true ]
      => apply beq_d_iff ; assumption
    | [H:  eq_d ?m ?n |- true = beq_d ?m ?n]
      => symmetry ; apply beq_d_iff ; assumption
    | [H: eq_d ?n ?m |- beq_d ?m ?n = true ] 
      => apply beq_d_iff ; symmetry ; assumption 
    | [H: eq_d ?n ?m |- true = beq_d ?m ?n ]
      => symmetry in H ; apply beq_d_iff in H ; assumption

    (* eq_var_vec clauses - symmetry permutations*)
    | [H: beq_var_vec ?m ?n = true |- eq_var_vec _ ?m ?n]
      => apply beq_var_vec_ok in H ; assumption
    | [H: true = beq_var_vec ?m ?n |- eq_var_vec _ ?m ?n]
      => symmetry in H ; apply beq_var_vec_ok in H ; assumption
    | [H: beq_var_vec ?m ?n = true |- eq_var_vec _ ?n ?m]
      => apply beq_var_vec_ok in H ; symmetry ; assumption 
    | [H: true = beq_var_vec ?m ?n |- eq_var_vec _ ?n ?m]
      => symmetry in H ; apply beq_var_vec_ok in H ; symmetry ; assumption
    (* beq_var_vecclauses - symmetry permutations*)
    | [H: eq_var_vec _ ?m ?n |- beq_var_vec ?m ?n = true ]
      => apply beq_var_vec_ok ; assumption
    | [H:  eq_var_vec _  ?m ?n |- true = beq_var_vec ?m ?n]
      => symmetry ; apply beq_var_vec_ok ; assumption
    | [H: eq_var_vec _ ?n ?m |- beq_var_vec ?m ?n = true ] 
      => apply beq_var_vec_ok ; symmetry ; assumption 
    | [H: eq_var_vec _ ?n ?m |- true = beq_var_vec ?m ?n ]
      => symmetry in H ; apply beq_var_vec_ok in H ; assumption

    (* eq_agent clauses - symmetry permutations*)
    | [H: beq_agent ?m ?n = true |- eq_agent ?m ?n]
      => apply beq_agent_iff in H ; assumption
    | [H: true = beq_agent ?m ?n |- eq_agent ?m ?n]
      => symmetry in H ; apply beq_agent_iff in H ; assumption
    | [H: beq_agent ?m ?n = true |- eq_agent ?n ?m]
      => apply beq_agent_iff in H ; symmetry ; assumption 
    | [H: true = beq_agent ?m ?n |- eq_agent ?n ?m]
      => symmetry in H ; apply beq_agent_iff in H ; symmetry ; assumption
    (* beq_agent clauses - symmetry permutations*)
    | [H: eq_agent ?m ?n |- beq_agent ?m ?n = true ]
      => apply beq_agent_iff ; assumption
    | [H:  eq_agent ?m ?n |- true = beq_agent ?m ?n]
      => symmetry ; apply beq_agent_iff ; assumption
    | [H: eq_agent ?n ?m |- beq_agent ?m ?n = true ] 
      => apply beq_agent_iff ; symmetry ; assumption 
    | [H: eq_agent ?n ?m |- true = beq_agent ?m ?n ]
      => symmetry in H ; apply beq_agent_iff in H ; assumption

    (* reflexivity clauses *)
    | [ |- beq_d ?d ?d = true]
      => apply beq_d_iff ; reflexivity 
    | [ |- eq_d ?d ?d ]
      => reflexivity
  end.



Record Predicate : Type := mkpredicate {
  name : pred_ident ; 
  arity : nat ;
  params : var_vec arity ; 
  body : Agent 
}.


Inductive eq_predicate : Predicate -> Predicate -> Prop :=
  | EqPred : forall pi1 pi2 a x1 x2 ag1 ag2 ,
                        eq_pred_ident pi1 pi2 
                   -> eq_var_vec a x1 x2
                   -> eq_agent ag1 ag2 
                   -> eq_predicate (mkpredicate pi1 a x1 ag1) (mkpredicate pi2 a x2 ag2).

Instance Eq_Predicate : Equivalence eq_predicate.
Proof.
  constructor ; [unfold Reflexive | unfold Symmetric | unfold Transitive].
  intros.
  depind x.
  apply EqPred ; reflexivity.
  intros.
  depind H.
  constructor ; try solve [symmetry ; assumption].
  depind x ; depind y ; intros.
  depind H.
  depind z ; depind H0 ; intros.
  apply EqPred.
  apply transitivity with (y := name1) ; auto.
  apply transitivity with (y := params1) ; auto.
  apply transitivity with (y := body1) ; auto.
Qed.

Definition beq_predicate (pred pred' : Predicate) : bool :=
   (beq_pred_ident (name pred) (name pred')) 
&& (beq_nat (arity pred) (arity pred')) 
&& (beq_var_vec (params pred) (params pred'))
&& (beq_agent (body pred) (body pred')).

Lemma beq_predicate_iff : forall pred pred', beq_predicate pred pred' = true <-> eq_predicate pred pred'.
Proof.
  intros ; split ; intros ; 
    depind pred ; destruct pred'. 
    unfold beq_predicate in H.
    andb_simpl.
    simpl in *.
    apply beq_nat_true_iff in H2 ; subst.
    constructor ;
    beq_eq_solv.

    depind H ;
      unfold beq_predicate ; simpl ;
      andb_simpl ; beq_eq_solv.
Qed.


Definition Program := list Predicate.

(* list remove for programs - 
can't use list-remove because the type of the decidable equality uses '=' *)
Fixpoint prog_remove (pred : Predicate) (prog : Program) : Program :=
  match prog with
    | nil    => nil
    | (pred' :: prog') => if beq_predicate pred pred' then prog' else (pred' :: (prog_remove pred prog'))
  end.

Fixpoint prog_lookup (p : pred_ident) (prog : Program) : option Predicate :=
  match prog with
    | nil   => None
    | (pred :: prog') => if beq_pred_ident p (name pred) then Some pred else prog_lookup p prog'
  end.

(* -------------------------------------------------- *)

(* ==================== SEMANTICS =================== *)
                     
Definition Poly_d := Agent -> D -> D.
Definition poly_d_bot := fun (a : Agent) (d : D) => d_bot.

Inductive lt_poly_d : Poly_d -> Poly_d -> Prop :=
  | LT_Poly_d : forall f f',
                 (forall a d, blt_d (f a d) (f' a d) = true)
              -> lt_poly_d f f'.

Lemma lt_poly_d_bot : forall (f : Poly_d), lt_poly_d poly_d_bot f. 
Proof.
  intros ; constructor ; intros.
  unfold poly_d_bot ; simpl.
  apply d_bot_bot.
Qed.

Parameter lt_poly_d_refl : forall f , lt_poly_d f f.
Parameter lt_poly_d_trans : forall f f' f'', lt_poly_d f f' -> lt_poly_d f' f'' -> lt_poly_d f f''.


(* See Paper, definition 3 *)
Fixpoint Fpd (prog : Program) (f : Poly_d) (a : Agent) : D -> D.
refine (
  match a with
    | A_ask d'  => fun d => if blt_d d d' then d else d_top   
    | A_conj a b => fun d => f b (f a d)
    | A_sum a b  => fun d => join (f a d) (f b d) 
    | A_head n p x   => fun d => match (prog_lookup p prog) with
                                 | None      => d_bot
                                 | Some pred => _ 
                               end
  end
).

remember (beq_nat n (arity pred)).
destruct b.
refine (                            (e_proj x d)
).
apply d_bot.
Defined.
Require Program.Wf.


(* THIS IS WHERE THE PROBLEM IS *)
Lemma Prop1 : forall (prog : Program) (p : pred_ident) {n : nat} (x : var_vec n) (d : D),
                          lt_d  (Fpd prog poly_d_bot (A_head p x) d) d_top.
Proof.                     
  intros.
  unfold not in *.
  intros.
  remember (prog_lookup p prog).
  destruct o.
  
Focus 2.
(* HERE *)
simpl.
  compute.
  simpl.
  unfold Fpd. 
  simpl.