The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

What about adding the original value as an explicit parameter? I.e. something like

Definition andl (l : list Prop) : Prop :=

  fold_right and True l.

Fixpoint foo (c orig : C) : Prop :=

  match c with

  | Build_C la =>

    andl (map (fun a =>

                 match a with

                 | Build_A cp =>

                   match cp with

                   | inl c' => foo c' orig

                   | inr p => exists u : U, In u (f orig)

                   end

                 end)

              la)

  end.

(I replaced the "In" premise with an explicit conjunction to please the guard checker). 

2014-01-29 Terrell, Jeffrey <jeffrey.terrell AT kcl.ac.uk>

I'm having difficult writing a recursive specification that would generate the nested set of match statements below. The problem is that I want to reason about the original value of c whenever the recursion terminates, and not the current value of c. For example, in the inr p3 branch, I want to reason about c1, not c3; and in the inr p2 branch, I want to reason about c1, not c2; and so on.

 

Any help would be much appreciated. Thanks.

 

Require Import List.

 

Inductive C : Set :=
   Build_C : list A -> C
with A : Set :=
   Build_A : C + P -> A
with P : Set :=
   Build_P : P.

 

Inductive T : Set :=
   Build_T : list U -> T
with U : Set :=
   Build_U : U.

 

Variable f : C -> list U.
Variable c1 : C.

 

Check

(* 1 *)
match c1 with Build_C la1 =>
   forall a1 : A, In a1 la1 ->
      match a1 with Build_A cp1 =>
         match cp1 with
            inl c2 =>
               (* 2 *)
               match c2 with Build_C la2 =>
                  forall a2 : A, In a2 la2 ->
                     match a2 with Build_A cp2 =>
                        match cp2 with
                           inl c3 =>
                              (* 3 *)
                              match c3 with Build_C la3 =>
                                 forall a3 : A, In a3 la3 ->
                                    match a3 with Build_A cp3 =>
                                       match cp3 with
                                          inl c4 => (* 4 *) ... |
                                          inr p3 => exists u : U, In u (f c1)
                                       end
                                    end
                              end |
                           inr p2 => exists u : U, In u (f c1)
                        end
                     end
                  end |
            inr p1 => exists u : U, In u (f c1)
         end
      end
end.

 

Regards,

Jeff.

--
Arthur Azevedo de Amorim