coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] proof with as

From: Patricia Peratto <psperatto AT vera.com.uy>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] proof with as
Date: Mon, 17 May 2021 14:55:30 -0300 (UYT)
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=psperatto AT vera.com.uy; spf=Pass smtp.mailfrom=psperatto AT vera.com.uy; spf=None smtp.helo=postmaster AT mail.vera.com.uy
Dkim-filter: OpenDKIM Filter v2.9.0 mta04.in.vera.com.uy F08732225EC
Ironport-hdrordr: A9a23:suIlK677InTapllwJAPXwPDXdLJyesId70hD6qkRc20zTiT7//rDoB1/73DJYVkqNk3I9ergBEDEewK/yXcX2/h0AV7BZniEhILAFugLhuGO/9SKIVyaygcp79YZT0EIMqyIMbEVt6bHCV6DYrAd/OU=
Ironport-phdr: A9a23:HYBcnB/uUVWS8f9uWce8ngc9DxPPW53KNwIYoqAql6hJOvz6uci7bQqFu6gm1QaVFazgqNt8w9LMtK7hXWFSqb2gi1slNKJ2ahkelM8NlBYhCsPWQWfyLfrtcjBoVJ8aDAwt8H60K1VaF9jjbFPOvHKy8SQSGhLiPgZpO+j5AIHfg9mz2uyo5ZHeYgVFiDWgbb9vIxi9sBncuNQRjYZ+MKg61wHHomFPe+RYxGNoIUyckhPh7cqu/5Bt7jpdtes5+8FPTav1caI4TadFDDs9KGA6+NfrtRjYQgSR4HYXT3gbnQBJAwjB6xH6Q4vxvy7nvedzxCWWIcv7Rq0yVD+/7alkVQXohT8JOTA57m/Zic5/gr9Urx29phx/35XZb5uJOPViZazRYc8WSGhHU81MVyJBGIS8b44XAuQbJ+lYs5P9p1oSohu/HwanGfnhxSFShnDswa06z+MhGhzB0Qw4BNIOqGrbrM/vO6cOTeC1y7LFzSvdYPNMwzjx8pTHchckof2WQLJxcdPcxE8yHAzKklues5bqPy+J1usTqWib6fJtWOKxhmI6pA9/ojeiy9kwhoTIgo8Z1l7J+ytkzIorOdG2SE92b96gHZdOqS2XOZV6T8MtTWxrpSs3178LtJ6mcSUM1Z8pxAbfZuSZf4SU/h7vTumcLStiiH9rZb6znRm//Em4xuHhVMS4zkxGojRKn9XWuH0Bygbf58aZRvZ740yvwyyA1xrJ5eFBOU00lbTUK5omwrMok5ocq0XDHivslEXokqCWbF8r9vK05OTgZ7XqvIKcNo9shgH/NKQhhNC/DPwmPgQSQ2SX4+ux2KH58UD3XblGlPI7n6jBvJDfP8sbp6q5AwFP0oYk7hayFy+m0M8AnXYZNlJKYg6Hj5TuO1zVPvD3E+2/jE62nDh3wPDGO6ftAojNL3TbirfuYa5961JAyAo01d1Q+5VUCqgYLP3vXk/xqcfXAwQiMw20xubnEM9y2pkfWWKJGK+ZMbndvUWG5uI1cKGwY9oevy+4IPw47ba6hngg3FQZYKOB3J0NaXn+EO4wcGuDZn+5ut4dC2YBvwN2dOHwgUGeVnYHf22qUrg1+i08IJyrF46FTYeoxqGQinToVqZKb3xLXwjfWUzjcJ+JDq9kgMO6J8ZglnoaWKKoDYQm0FezpV2io1KCBvTZ4CRevpXmksVktbW7ff4a6zFuBoKW1GTLUnAmxws1

I have proved a theorem:

Theorem neq_nil_cons (A:Type(x:A)(y:list A)(z:list A)(p:cons x y = z): not (z=nil).

I have a Fixpoint:

Fixpoint proof1 (A:Type)(l:list A) :=

match l with

| x :: (y :: s) as ys => neq_nil_cons A y s ys H0

| _ => something

end.

In the place of H0 I need a proof that (cons y s)=ys.

How I can do this?

Regards,

Patricia

[Coq-Club] proof with as, Patricia Peratto, 05/17/2021
- Re: [Coq-Club] proof with as, Dominique Larchey-Wendling, 05/18/2021
- Re: [Coq-Club] proof with as, Christopher Ernest Sally, 05/18/2021