For the automation of tests in Coq, when is it appropriate to use canonical structures or dependent types instead of Ltac?

There are some possible approaches to automate testing in modern Coq.

  • Writing test scripts with Ltac. This is the approach described in, which the author uses with great success in projects such as It can significantly reduce the amount of test code required, but requires good handling of Ltac's peculiarities and does not seem easy to debug.
  • Automation based on canonical structures. This is the approach described in, and it is used in Mathcomp. It involves taking advantage of the Coq type inference mechanism to automatically run logical programs that search for certain types of test terms. It is described in that document as less ad-hoc than the Ltac-heavy approach, but not necessarily quicker, and may be more detailed due to the need to use the mechanism of canonical structures for something that was not designed directly. .
  • Dependent types / equations. The complement of Equations ( seems to facilitate in Coq the same convenience when working with programs written in a dependent manner as a language like Agda or Idris. With this approach, the processor acts as a form of automation, and the amount of test code is reduced by having the algorithms create, manipulate and transmit the terms of the test directly.

There are also some modern developments that complement these.

  • Ltac2. This is intended to be a replacement for Ltac, with fewer quirks and potentially better performance, as described in The document states that "Ltac2 is still in an active development phase, but the basics of the language have been established.Most of all, users are needed to polish the rough edges". If it is intended to be a replacement superior to Ltac, should it be considered in lieu of Ltac for new projects, since it is already ready for user testing?
  • Metacoq This provides meta-programming functions that allow the development of higher-level tools, as described in, and presumably simplify the use of the test by reflection, Technique used in approaches based on both canonical and Ltac-heavy structures.

My question is, if I am starting a new project, what criteria should I use to determine which approach or combination of them to adopt? As a concrete example, imagine that I want to verify the easy-to-verify parts of a program that connects to a server through the Internet, downloads some data, processes the data in some way and then serves the processed data through TCP. By easy to verify I mean not verifying the TCP / HTTP stack, or trying from scratch to correct the known algorithms used in data processing. When I consider how I would structure this, it seems that the structure would be quite different depending on which of the previous approaches I used, and I lack the experience to make a judgment about which would produce the best result in terms of maximizing production. of verified code per unit of development time. What factors should require the use of canonical structures or equations instead of just a single Ltac?

seo – How to mark canonical labels for multiple versions of the same product?

We have a car research website where we have product pages. In addition, few products have some different variants with subtle differences. The case is similar to that of amazon iphone.

If you click on a different size (64, 128 and 256), they have three different URLs with different canonical characters. The content of these 3 pages is very identical, is it not duplicate content? Why does not Google penalize you for this duplicity?

Also, if I write ranges of iphone pages XR – 64 gb, if I write ranges of pages iphone xr 64 gb – again 64 gb, if I write ranges of iphone pages xr 128 gb – 128 gb. How do you identify that 64 GB should be prioritized?

Also, I do not see anything defined as such in the structured data.

Can someone tell me how this is happening? Also, what should be URL and canonical for such products?

redirects – Canonical labels on redirects of forms pages

I am adding canonical tags to our website and I would like to add them to the pages where users can download guides, but depending on the user's configuration, they could be redirected.

If they are cooked, they would go directly to the canonical url, eg. / downloads / product-white paper

If they are new users, they are redirected to a page with a form field to provide information before downloading. This page has an event code in the URL. / downloads / lituraturemain? event = ABC-123-DEF-456

What are the best practices for adding canonical labels in a situation like this?

seo – 301 Redirect vs Canonical Link – which one is preferred?

Let's say I have the following three URLs.

            Url1: Domain / Start
Url2: www.dominio/ inicio
Url3: domain / home <- Canonical

With respect to SEO, is it preferable to add a canonical link to Url1 and Url2, or is it better to do a Redirect 301 to Url3 when the user visits Url1 and Url2?

I'm looking for the best SEO practice.

development: disable the redirection to the canonical domain (or to the host website in any hostname)

I want to have several developments and trial environments of a WordPress multisite ( Because of this, it would be great if WordPress did not redirect to what it considers the canonical domain name.

I'm having problems with this in my wp-config.php:

define (& # 39; DOMAIN_CURRENT_SITE & # 39 ;, gethostname ());

Redirects to or it gives me errors in the database.

This is after wp search-replace

Is it possible to deactivate this redirection? If so, how?

seo – Should I include the file extensions in the canonical links?

I sent a page to the Google Search Console and I received an error message "Duplicate without the canon selected by the user".

The full URL is but I want it to appear without the file extension in the Google search results.

So I included the canonical link in the tab below. ">

I have seen several articles included in a Moz blog that showed canonical links without file extensions.

So, do I have to include the file extension in the canonical link?

How can I tell Google that I do not want to display .html in Google search results?

Google selected a URL without a file extension for another of my pages, so it seems that the answer to my question is no.

However, in the new canonical URL chosen by Google, they added "www". before the URL. I do not include "www". in my URLs and I do not want Google to show "www". in the search result

I thought that the whole purpose of canonical links is to tell Google the URL you use to access and display a page in the search results. What good is it if Google allocates canonical URLs different from the ones you provide?

Try canonical greedy coin algorithm

I am trying to prove the following:

Show that for the next S coin system, the following greedy algorithm offers the optimal solution:
Select the largest possible currency in each step until the amount of money has been obtained for any given value of money.
S = {1,2,5,10,20,50,100,200}.

I do not know where to start with this test. I'm thinking that mathematical induction could be used, but I'm not sure how I would perform that test. This problem is very easy to test for particular amounts of money, but I have no idea how to test it for any amount of money.

htaccess – canonical rel for http and https

Simply configure the canon to the HTTPS version (preferred). Both HTTP and HTTPS will remain available. Anyway, Google will probably favor the HTTPS version over HTTP, regardless of the protocol it establishes in rel = "canonical" label (because presumably you will know that both HTTPS and HTTP are available).

Setting the canonical conditional condition based on the protocol makes no sense: Are HTTP and HTTPS probably serving the same content? You can not have two different "canonical URLs" for the same content.

Differential geometry – Form of canonical welding and torsion.

Leave $ FOM $ be the orthogonal frame package, $ theta: FOM to V $, with $ V $ A vector space equipped with the Minkowski metric. $ eta $, its welding. It is true that $ theta $ Is it canonical welding?

At this point I can define the shape of torsion, I define it as

$$ T = d_ omega theta = d theta + omega wedge_f theta $$

where $ d_ omega $ It is the covariant derivative in the fundamental representation. A) Yes $ ( omega wedge_f theta) ^ {ad} = omega ^ {ab} wedge theta ^ {cd} eta_ {bc} $. Is this definition the most general? Could you define the torsion in a generic representation?

Any reference would be appreciated, thanks!

seo: the AMP (404) URL was not found in Google Webmaster Tools, but the AMP / Canonical pages work well

Webmaster Tools has been reporting 404 errors on several of my AMP pages since last month. The number of pages affected changes every 24 hours, and now it is increasing every day, which is killing my mobile traffic.

Test the live URL: it works well on each page reported, the page recovery was successful, indexing is allowed, the linked version of AMP is valid

The canonical link works, the AMP link works, the Smartphone robot is the only one that seems to be confused.

View post on

Any help finding a resolution would be greatly appreciated, because from now on, my web traffic is dying quickly due to these problems. Here are a couple of the URLs reported …