Hello Abid,
The term quotation fails type checking simply because the types of LHS
and RHS of the equality are different:
`:real^((N,P)finite_sum,Q)finite_sum^M` (with type vars N, P, Q, M)
`:real^(N,(P,Q)finite_sum)finite_sum^M` (with type vars N, P, Q, M)
As I understand it (I may be wrong here), there is no way of getting the
HOL type system to let you express this associativity property about
'horz_conct1'. If you want to express these kinds of properties, I
think you need to define your function in a different way, not using
types like this.
Mark.
On 02/07/2016 10:30, Abid Rauf wrote:
> Dear All,
>
> I am having the following type checking issue with a definition in the Matrix
> theory of HOL-Light. It seems the double application of the function leads to
> an unknown dimension of the matrix, which is causing the problem. I would
> appreciate if someone can please help me out with us.
>
> let horz_conct1 = new_definition
> `(horz_conct1:real^N^M->real^P^M->real^((N,P)finite_sum)^M) A B = lambda a b
> .
> if (b<=dimindex(:N))
> then (A$a$b) else (B$a$(b-(dimindex(:N))))`;;
>
> Now if i want to prove that
>
> g`!(A:real^N^M) (B:real^P^M) (C:real^Q^M). horz_conct1 (horz_conct1 A B) (C)=
> horz_conct1 (A) (horz_conct1 B C)`;;
>
> it gives following error
>
> Exception: Failure "typechecking error (initial type assignment)".
>
> So the definition is accepted but the proof goal using the function gives the
> problem.
>
> Best Regards,
>
> Abid Rauf
> Ph.D Scholar (CS) & RA SAVe Labs,
> School of Electrical Engineering and Computer Science (SEECS),
> National University of Science and Technology (NUST), H-12, Islamabad,
> Pakistan
> ------------------------------------------------------------------------------
> Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
> Francisco, CA to explore cutting-edge tech and listen to tech luminaries
> present their vision of the future. This family event has something for
> everyone, including kids. Get more information and register today.
> http://sdm.link/attshape
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
Francisco, CA to explore cutting-edge tech and listen to tech luminaries
present their vision of the future. This family event has something for
everyone, including kids. Get more information and register today.
http://sdm.link/attshape
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
